Theorem bj-velpwALT 37108

Description: This theorem bj-velpwALT 37108 and the next theorem bj-elpwgALT 37109 are alternate proofs of velpw 4556 and elpwg 4554 respectively, where one proves first the setvar case and then generalizes using vtoclbg 3512 instead of proving first the general case using elab2g 3633 and then specifying. Here, this results in needing an extra DV condition, a longer combined proof and use of ax-12 2182. In other cases, that order is better (e.g., vsnex 5376 proved before snexg 5377). (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 4553	. . 3 ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴}
2	1	eleq2i 2825	. 2 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ∈ {𝑥 ∣ 𝑥 ⊆ 𝐴})
3		abid 2715	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝑥 ⊆ 𝐴} ↔ 𝑥 ⊆ 𝐴)
4	2, 3	bitri 275	1 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)

Syntax hints:   ↔ wb 206   ∈ wcel 2113  {cab 2711   ⊆ wss 3899  𝒫 cpw 4551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-pw 4553

This theorem is referenced by:  bj-elpwgALT  37109