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 36016
Description: Alternate proof of pw0 4815. The proofs have a similar structure: pw0 4815 uses the definitions of powerclass and singleton as class abstractions, whereas bj-pw0ALT 36016 uses characterizations of their elements. Both proofs then use transitivity of a congruence relation (equality for pw0 4815 and biconditional for bj-pw0ALT 36016) to translate the property ss0b 4397 into the wanted result. To translate a biconditional into a class equality, pw0 4815 uses abbii 2802 (which yields an equality of class abstractions), while bj-pw0ALT 36016 uses eqriv 2729 (which requires a biconditional of membership of a given setvar variable). Note that abbii 2802, through its closed form abbi 2800, is proved from eqrdv 2730, which is the deduction form of eqriv 2729. In the other direction, velpw 4607 and velsn 4644 are proved from the definitions of powerclass and singleton using elabg 3666, which is a version of abbii 2802 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 4397 . . 3 (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2 velpw 4607 . . 3 (𝑥 ∈ 𝒫 ∅ ↔ 𝑥 ⊆ ∅)
3 velsn 4644 . . 3 (𝑥 ∈ {∅} ↔ 𝑥 = ∅)
41, 2, 33bitr4i 302 . 2 (𝑥 ∈ 𝒫 ∅ ↔ 𝑥 ∈ {∅})
54eqriv 2729 1 𝒫 ∅ = {∅}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  wcel 2106  wss 3948  c0 4322  𝒫 cpw 4602  {csn 4628
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3951  df-in 3955  df-ss 3965  df-nul 4323  df-pw 4604  df-sn 4629
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator