---

Step * 1 of Lemma isect2-b-union-subtype

.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. C : Type
4. ¬B ⋂ C
5. x : A ⋂ B ⋃ C@i
⊢ x ∈ A ⋂ B ⋃ A ⋂ C
BY
{ Assert ⌜∃y:B ⋃ C. (y = x ∈ (B ⋃ C))⌝⋅ }

1
.....assertion..... 
1. A : Type
2. B : Type
3. C : Type
4. ¬B ⋂ C
5. x : A ⋂ B ⋃ C@i
⊢ ∃y:B ⋃ C. (y = x ∈ (B ⋃ C))

2
1. A : Type
2. B : Type
3. C : Type
4. ¬B ⋂ C
5. x : A ⋂ B ⋃ C@i
6. ∃y:B ⋃ C. (y = x ∈ (B ⋃ C))
⊢ x ∈ A ⋂ B ⋃ A ⋂ C

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  \mneg{}B  \mcap{}  C
5.  x  :  A  \mcap{}  B  \mcup{}  C@i
\mvdash{}  x  \mmember{}  A  \mcap{}  B  \mcup{}  A  \mcap{}  C


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}y:B  \mcup{}  C.  (y  =  x)\mkleeneclose{}\mcdot{}

---

Home Index