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

Theorem bj-velpwALT 37036
Description: This theorem bj-velpwALT 37036 and the next theorem bj-elpwgALT 37037 are alternate proofs of velpw 4610 and elpwg 4608 respectively, where one proves first the setvar case and then generalizes using vtoclbg 3557 instead of proving first the general case using elab2g 3683 and then specifying. Here, this results in needing an extra DV condition, a longer combined proof and use of ax-12 2175. In other cases, that order is better (e.g., vsnex 5440 proved before snexg 5441). (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
bj-velpwALT (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem bj-velpwALT
StepHypRef Expression
1 df-pw 4607 . . 3 𝒫 𝐴 = {𝑥𝑥𝐴}
21eleq2i 2831 . 2 (𝑥 ∈ 𝒫 𝐴𝑥 ∈ {𝑥𝑥𝐴})
3 abid 2716 . 2 (𝑥 ∈ {𝑥𝑥𝐴} ↔ 𝑥𝐴)
42, 3bitri 275 1 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wcel 2106  {cab 2712  wss 3963  𝒫 cpw 4605
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-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-pw 4607
This theorem is referenced by:  bj-elpwgALT  37037
  Copyright terms: Public domain W3C validator