---

Step * 1 1 of Lemma isect_prod_lemma


1. A : Type
2. B : Type
3. C : Type
4. x : A × B ⋂ A × C
5. x ∈ A × C
6. x ∈ A × B
⊢ x ∈ A × B ⋂ C
BY
{ Subst x ~ <fst(x), snd(x)> 0 }

1
.....equality..... 
1. A : Type
2. B : Type
3. C : Type
4. x : A × B ⋂ A × C
5. x ∈ A × C
6. x ∈ A × B
⊢ x ~ <fst(x), snd(x)>

2
1. A : Type
2. B : Type
3. C : Type
4. x : A × B ⋂ A × C
5. x ∈ A × C
6. x ∈ A × B
⊢ <fst(x), snd(x)> ∈ A × B ⋂ C

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  x  :  A  \mtimes{}  B  \mcap{}  A  \mtimes{}  C
5.  x  \mmember{}  A  \mtimes{}  C
6.  x  \mmember{}  A  \mtimes{}  B
\mvdash{}  x  \mmember{}  A  \mtimes{}  B  \mcap{}  C


By

---

Latex:
Subst  x  \msim{}  <fst(x),  snd(x)>  0

---

Home Index