Theorem bj-velpwALT 37292

Description: This theorem bj-velpwALT 37292 and the next theorem bj-elpwgALT 37293 are alternate proofs of velpw 4561 and elpwg 4559 respectively, where one proves first the setvar case and then generalizes using vtoclbg 3516 instead of proving first the general case using elab2g 3637 and then specifying. Here, this results in needing an extra DV condition, a longer combined proof and use of ax-12 2185. In other cases, that order is better (e.g., vsnex 5381 proved before snexg 5386). (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

Step	Hyp	Ref	Expression
1		df-pw 4558	. . 3 ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴}
2	1	eleq2i 2829	. 2 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ∈ {𝑥 ∣ 𝑥 ⊆ 𝐴})
3		abid 2719	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝑥 ⊆ 𝐴} ↔ 𝑥 ⊆ 𝐴)
4	2, 3	bitri 275	1 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)

Syntax hints:   ↔ wb 206   ∈ wcel 2114  {cab 2715   ⊆ wss 3903  𝒫 cpw 4556

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-pw 4558

This theorem is referenced by:  bj-elpwgALT  37293