Theorem bj-pw0ALT 34358

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

Assertion

Ref	Expression
bj-pw0ALT	⊢ 𝒫 ∅ = {∅}

Proof of Theorem bj-pw0ALT

Step	Hyp	Ref	Expression
1		ss0b 4337	. . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2		velpw 4530	. . 3 ⊢ (𝑥 ∈ 𝒫 ∅ ↔ 𝑥 ⊆ ∅)
3		velsn 4569	. . 3 ⊢ (𝑥 ∈ {∅} ↔ 𝑥 = ∅)
4	1, 2, 3	3bitr4i 305	. 2 ⊢ (𝑥 ∈ 𝒫 ∅ ↔ 𝑥 ∈ {∅})
5	4	eqriv 2818	1 ⊢ 𝒫 ∅ = {∅}

Syntax hints:   = wceq 1537   ∈ wcel 2114   ⊆ wss 3924  ∅c0 4279  𝒫 cpw 4525  {csn 4553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3488  df-dif 3927  df-in 3931  df-ss 3940  df-nul 4280  df-pw 4527  df-sn 4554

This theorem is referenced by: (None)