Theorem bj-pw0ALT 34370

Description: Alternate proof of pw0 4738. The proofs have a similar structure: pw0 4738 uses the definitions of powerclass and singleton as class abstractions, whereas bj-pw0ALT 34370 uses characterizations of their elements. Both proofs then use transitivity of a congruence relation (equality for pw0 4738 and biconditional for bj-pw0ALT 34370) to translate the property ss0b 4344 into the wanted result. To translate a biconditional into a class equality, pw0 4738 uses abbii 2885 (which yields an equality of class abstractions), while bj-pw0ALT 34370 uses eqriv 2817 (which requires a biconditional of membership of a given setvar variable). Note that abbii 2885, through its closed form abbi1 2883, is proved from eqrdv 2818, which is the deduction form of eqriv 2817. In the other direction, velpw 4537 and velsn 4576 are proved from the definitions of powerclass and singleton using elabg 3662, which is a version of abbii 2885 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 4344	. . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2		velpw 4537	. . 3 ⊢ (𝑥 ∈ 𝒫 ∅ ↔ 𝑥 ⊆ ∅)
3		velsn 4576	. . 3 ⊢ (𝑥 ∈ {∅} ↔ 𝑥 = ∅)
4	1, 2, 3	3bitr4i 305	. 2 ⊢ (𝑥 ∈ 𝒫 ∅ ↔ 𝑥 ∈ {∅})
5	4	eqriv 2817	1 ⊢ 𝒫 ∅ = {∅}

Syntax hints:   = wceq 1536   ∈ wcel 2113   ⊆ wss 3929  ∅c0 4284  𝒫 cpw 4532  {csn 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-v 3493  df-dif 3932  df-in 3936  df-ss 3945  df-nul 4285  df-pw 4534  df-sn 4561

This theorem is referenced by: (None)