---

Step * of Lemma setimages_functionality

∀b1,b2,x1,x2:coSet{i:l}.  (seteq(b1;b2) ⇒ seteq(x1;x2) ⇒ seteq(setimages(b1;x1);setimages(b2;x2)))
BY
{ (Auto
   THEN ((RWO  "co-seteq-iff" 0 THENM D 0) THENA Auto)
   THEN (Assert ∀z:coSet{i:l}. ((z ∈ b1) ⇐⇒ (z ∈ b2)) BY
               (RWO "-3" 0 THEN Auto))) }

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

---

Latex:

---

Latex:
\mforall{}b1,b2,x1,x2:coSet\{i:l\}.    (seteq(b1;b2)  {}\mRightarrow{}  seteq(x1;x2)  {}\mRightarrow{}  seteq(setimages(b1;x1);setimages(b2;x2)))


By

---

Latex:
(Auto
  THEN  ((RWO    "co-seteq-iff"  0  THENM  D  0)  THENA  Auto)
  THEN  (Assert  \mforall{}z:coSet\{i:l\}.  ((z  \mmember{}  b1)  \mLeftarrow{}{}\mRightarrow{}  (z  \mmember{}  b2))  BY
                          (RWO  "-3"  0  THEN  Auto)))

---

Home Index