---

Step * of Lemma seteq-orderedpairs-iff

∀a,b,a',b':coSet{i:l}.  (seteq((a,b);(a',b')) ⇐⇒ seteq(a;a') ∧ seteq(b;b'))
BY
{ (Intros THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. a : coSet{i:l}
2. b : coSet{i:l}
3. a' : coSet{i:l}
4. b' : coSet{i:l}
5. seteq((a,b);(a',b'))
⊢ seteq(a;a') ∧ seteq(b;b')

2
1. a : coSet{i:l}
2. b : coSet{i:l}
3. a' : coSet{i:l}
4. b' : coSet{i:l}
5. seteq(a;a') ∧ seteq(b;b')
⊢ seteq((a,b);(a',b'))

---

Latex:

---

Latex:
\mforall{}a,b,a',b':coSet\{i:l\}.    (seteq((a,b);(a',b'))  \mLeftarrow{}{}\mRightarrow{}  seteq(a;a')  \mwedge{}  seteq(b;b'))


By

---

Latex:
(Intros  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index