Theorem bj-pw0ALT

Description: Alternate proof of pw0 . The proofs have a similar structure: pw0 uses the definitions of powerclass and singleton as class abstractions, whereas bj-pw0ALT uses characterizations of their elements. Both proofs then use transitivity of a congruence relation (equality for pw0 and biconditional for bj-pw0ALT ) to translate the property ss0b into the wanted result. To translate a biconditional into a class equality, pw0 uses abbii (which yields an equality of class abstractions), while bj-pw0ALT uses eqriv (which requires a biconditional of membership of a given setvar variable). Note that abbii , through its closed form abbi , is proved from eqrdv , which is the deduction form of eqriv . In the other direction, velpw and velsn are proved from the definitions of powerclass and singleton using elabg , which is a version of abbii suited for membership characterizations. (Contributed by BJ, 14-Apr-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-pw0ALT	$$⊢𝒫\varnothing =\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		ss0b	$$⊢x\subseteq \varnothing \leftrightarrow x=\varnothing$$
2		velpw	$$⊢x\in 𝒫\varnothing \leftrightarrow x\subseteq \varnothing$$
3		velsn	$$⊢x\in \left\{\varnothing \right\}\leftrightarrow x=\varnothing$$
4	1 2 3	3bitr4i	$$⊢x\in 𝒫\varnothing \leftrightarrow x\in \left\{\varnothing \right\}$$
5	4	eqriv	$$⊢𝒫\varnothing =\left\{\varnothing \right\}$$