---

Step * of Lemma equipollent-sets

∀[T:Type]. ∀[P,Q:T ⟶ ℙ].  {x:T| P[x]}  ~ {x:T| Q[x]}  supposing ∀x:T. (P[x] ⇐⇒ Q[x])
BY
{ (Auto THEN BLemma `equipollent_weakening_ext-eq` THEN Auto) }

1
1. T : Type
2. P : T ⟶ ℙ
3. Q : T ⟶ ℙ
4. ∀x:T. (P[x] ⇐⇒ Q[x])
⊢ {x:T| P[x]}  ≡ {x:T| Q[x]} 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P,Q:T  {}\mrightarrow{}  \mBbbP{}].    \{x:T|  P[x]\}    \msim{}  \{x:T|  Q[x]\}    supposing  \mforall{}x:T.  (P[x]  \mLeftarrow{}{}\mRightarrow{}  Q[x])


By

---

Latex:
(Auto  THEN  BLemma  `equipollent\_weakening\_ext-eq`  THEN  Auto)

---

Home Index