---

Step * 1 of Lemma allsetmem_functionality


1. A : coSet{i:l}
2. P : {a:coSet{i:l}| (a ∈ A)}  ⟶ ℙ
3. B : coSet{i:l}
4. set-predicate{i:l}(A;a.P[a])
5. seteq(A;B)
6. set-predicate{i:l}(B;a.P[a])
⊢ ∀a∈A.P[a] ⇐⇒ ∀a∈B.P[a]
BY
{ (RWO  "allsetmem-iff" 0 THENA (Auto THEN MemTypeCD THEN Auto THEN RWO "5" 0 THEN Auto)) }

1
1. A : coSet{i:l}
2. P : {a:coSet{i:l}| (a ∈ A)}  ⟶ ℙ
3. B : coSet{i:l}
4. set-predicate{i:l}(A;a.P[a])
5. seteq(A;B)
6. set-predicate{i:l}(B;a.P[a])
⊢ ∀a:coSet{i:l}. ((a ∈ A) ⇒ P[a]) ⇐⇒ ∀a:coSet{i:l}. ((a ∈ B) ⇒ P[a])

---

Latex:

---

Latex:

1.  A  :  coSet\{i:l\}
2.  P  :  \{a:coSet\{i:l\}|  (a  \mmember{}  A)\}    {}\mrightarrow{}  \mBbbP{}
3.  B  :  coSet\{i:l\}
4.  set-predicate\{i:l\}(A;a.P[a])
5.  seteq(A;B)
6.  set-predicate\{i:l\}(B;a.P[a])
\mvdash{}  \mforall{}a\mmember{}A.P[a]  \mLeftarrow{}{}\mRightarrow{}  \mforall{}a\mmember{}B.P[a]


By

---

Latex:
(RWO    "allsetmem-iff"  0  THENA  (Auto  THEN  MemTypeCD  THEN  Auto  THEN  RWO  "5"  0  THEN  Auto))

---

Home Index