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 abbi1 , 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	⊢ 𝒫 ∅ = { ∅ }

Proof

Step	Hyp	Ref	Expression
1		ss0b	⊢ ( 𝑥 ⊆ ∅ ↔ 𝑥 = ∅ )
2		velpw	⊢ ( 𝑥 ∈ 𝒫 ∅ ↔ 𝑥 ⊆ ∅ )
3		velsn	⊢ ( 𝑥 ∈ { ∅ } ↔ 𝑥 = ∅ )
4	1 2 3	3bitr4i	⊢ ( 𝑥 ∈ 𝒫 ∅ ↔ 𝑥 ∈ { ∅ } )
5	4	eqriv	⊢ 𝒫 ∅ = { ∅ }