Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-pw0ALT Structured version   Visualization version   GIF version

Theorem bj-pw0ALT 34463
Description: Alternate proof of pw0 4705. The proofs have a similar structure: pw0 4705 uses the definitions of powerclass and singleton as class abstractions, whereas bj-pw0ALT 34463 uses characterizations of their elements. Both proofs then use transitivity of a congruence relation (equality for pw0 4705 and biconditional for bj-pw0ALT 34463) to translate the property ss0b 4305 into the wanted result. To translate a biconditional into a class equality, pw0 4705 uses abbii 2863 (which yields an equality of class abstractions), while bj-pw0ALT 34463 uses eqriv 2795 (which requires a biconditional of membership of a given setvar variable). Note that abbii 2863, through its closed form abbi1 2861, is proved from eqrdv 2796, which is the deduction form of eqriv 2795. In the other direction, velpw 4502 and velsn 4541 are proved from the definitions of powerclass and singleton using elabg 3614, which is a version of abbii 2863 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
StepHypRef Expression
1 ss0b 4305 . . 3 (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2 velpw 4502 . . 3 (𝑥 ∈ 𝒫 ∅ ↔ 𝑥 ⊆ ∅)
3 velsn 4541 . . 3 (𝑥 ∈ {∅} ↔ 𝑥 = ∅)
41, 2, 33bitr4i 306 . 2 (𝑥 ∈ 𝒫 ∅ ↔ 𝑥 ∈ {∅})
54eqriv 2795 1 𝒫 ∅ = {∅}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wcel 2111  wss 3881  c0 4243  𝒫 cpw 4497  {csn 4525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898  df-nul 4244  df-pw 4499  df-sn 4526
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator