Step
*
1
of Lemma
union-set-is-set-exists
.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. P : A ⟶ B ⟶ ℙ
4. x : ⋃x:A.{y:B| P[x;y]} @i
⊢ x ∈ {y:B| ∃x:A. P[x;y]}
BY
{ (D_union (-1) THEN DVarSets THEN MemTypeCD THEN Auto) }
Latex:
Latex:
.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. P : A {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}
4. x : \mcup{}x:A.\{y:B| P[x;y]\} @i
\mvdash{} x \mmember{} \{y:B| \mexists{}x:A. P[x;y]\}
By
Latex:
(D\_union (-1) THEN DVarSets THEN MemTypeCD THEN Auto)
Home
Index