---

Step * of Lemma seteq-iff

∀s1,s2:Set{i:l}.  (seteq(s1;s2) ⇐⇒ ∀x:Set{i:l}. ((x ∈ s1) ⇐⇒ (x ∈ s2)))
BY
{ (Intros THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. s1 : Set{i:l}
2. s2 : Set{i:l}
3. seteq(s1;s2)
⊢ ∀x:Set{i:l}. ((x ∈ s1) ⇐⇒ (x ∈ s2))

2
1. s1 : Set{i:l}
2. s2 : Set{i:l}
3. ∀x:Set{i:l}. ((x ∈ s1) ⇐⇒ (x ∈ s2))
⊢ seteq(s1;s2)

---

Latex:

---

Latex:
\mforall{}s1,s2:Set\{i:l\}.    (seteq(s1;s2)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:Set\{i:l\}.  ((x  \mmember{}  s1)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  s2)))


By

---

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

---

Home Index