---

Step * of Lemma setmemfunclemma

∀x1,s1,x2,s2:coSet{i:l}.  (seteq(x1;x2) ⇒ seteq(s1;s2) ⇒ {(x1 ∈ s1) ⇐⇒ (x2 ∈ s2)})
BY
{ (Auto THEN (RWO "co-seteq-iff" (-1) THENA Auto) THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. x1 : coSet{i:l}
2. s1 : coSet{i:l}
3. x2 : coSet{i:l}
4. s2 : coSet{i:l}
5. seteq(x1;x2)
6. ∀z:coSet{i:l}. ((z ∈ s1) ⇐⇒ (z ∈ s2))
7. (x1 ∈ s1)
⊢ (x2 ∈ s2)

2
1. x1 : coSet{i:l}
2. s1 : coSet{i:l}
3. x2 : coSet{i:l}
4. s2 : coSet{i:l}
5. seteq(x1;x2)
6. ∀z:coSet{i:l}. ((z ∈ s1) ⇐⇒ (z ∈ s2))
7. (x2 ∈ s2)
⊢ (x1 ∈ s1)

---

Latex:

---

Latex:
\mforall{}x1,s1,x2,s2:coSet\{i:l\}.    (seteq(x1;x2)  {}\mRightarrow{}  seteq(s1;s2)  {}\mRightarrow{}  \{(x1  \mmember{}  s1)  \mLeftarrow{}{}\mRightarrow{}  (x2  \mmember{}  s2)\})


By

---

Latex:
(Auto  THEN  (RWO  "co-seteq-iff"  (-1)  THENA  Auto)  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index