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 37032
Description: Alternate proof of pw0 4817. The proofs have a similar structure: pw0 4817 uses the definitions of powerclass and singleton as class abstractions, whereas bj-pw0ALT 37032 uses characterizations of their elements. Both proofs then use transitivity of a congruence relation (equality for pw0 4817 and biconditional for bj-pw0ALT 37032) to translate the property ss0b 4407 into the wanted result. To translate a biconditional into a class equality, pw0 4817 uses abbii 2807 (which yields an equality of class abstractions), while bj-pw0ALT 37032 uses eqriv 2732 (which requires a biconditional of membership of a given setvar variable). Note that abbii 2807, through its closed form abbi 2805, is proved from eqrdv 2733, which is the deduction form of eqriv 2732. In the other direction, velpw 4610 and velsn 4647 are proved from the definitions of powerclass and singleton using elabg 3677, which is a version of abbii 2807 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 4407 . . 3 (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2 velpw 4610 . . 3 (𝑥 ∈ 𝒫 ∅ ↔ 𝑥 ⊆ ∅)
3 velsn 4647 . . 3 (𝑥 ∈ {∅} ↔ 𝑥 = ∅)
41, 2, 33bitr4i 303 . 2 (𝑥 ∈ 𝒫 ∅ ↔ 𝑥 ∈ {∅})
54eqriv 2732 1 𝒫 ∅ = {∅}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  wcel 2106  wss 3963  c0 4339  𝒫 cpw 4605  {csn 4631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-dif 3966  df-ss 3980  df-nul 4340  df-pw 4607  df-sn 4632
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator