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 37050
Description: Alternate proof of pw0 4812. The proofs have a similar structure: pw0 4812 uses the definitions of powerclass and singleton as class abstractions, whereas bj-pw0ALT 37050 uses characterizations of their elements. Both proofs then use transitivity of a congruence relation (equality for pw0 4812 and biconditional for bj-pw0ALT 37050) to translate the property ss0b 4401 into the wanted result. To translate a biconditional into a class equality, pw0 4812 uses abbii 2809 (which yields an equality of class abstractions), while bj-pw0ALT 37050 uses eqriv 2734 (which requires a biconditional of membership of a given setvar variable). Note that abbii 2809, through its closed form abbi 2807, is proved from eqrdv 2735, which is the deduction form of eqriv 2734. In the other direction, velpw 4605 and velsn 4642 are proved from the definitions of powerclass and singleton using elabg 3676, which is a version of abbii 2809 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 4401 . . 3 (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2 velpw 4605 . . 3 (𝑥 ∈ 𝒫 ∅ ↔ 𝑥 ⊆ ∅)
3 velsn 4642 . . 3 (𝑥 ∈ {∅} ↔ 𝑥 = ∅)
41, 2, 33bitr4i 303 . 2 (𝑥 ∈ 𝒫 ∅ ↔ 𝑥 ∈ {∅})
54eqriv 2734 1 𝒫 ∅ = {∅}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wcel 2108  wss 3951  c0 4333  𝒫 cpw 4600  {csn 4626
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 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-ss 3968  df-nul 4334  df-pw 4602  df-sn 4627
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator