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 37054
Description: This theorem bj-velpwALT 37054 and the next theorem bj-elpwgALT 37055 are alternate proofs of velpw 4605 and elpwg 4603 respectively, where one proves first the setvar case and then generalizes using vtoclbg 3557 instead of proving first the general case using elab2g 3680 and then specifying. Here, this results in needing an extra DV condition, a longer combined proof and use of ax-12 2177. In other cases, that order is better (e.g., vsnex 5434 proved before snexg 5435). (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 4602 . . 3 𝒫 𝐴 = {𝑥𝑥𝐴}
21eleq2i 2833 . 2 (𝑥 ∈ 𝒫 𝐴𝑥 ∈ {𝑥𝑥𝐴})
3 abid 2718 . 2 (𝑥 ∈ {𝑥𝑥𝐴} ↔ 𝑥𝐴)
42, 3bitri 275 1 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wcel 2108  {cab 2714  wss 3951  𝒫 cpw 4600
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-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-pw 4602
This theorem is referenced by:  bj-elpwgALT  37055
  Copyright terms: Public domain W3C validator