Theorem bj-velpwALT 37486

Description: This theorem bj-velpwALT 37486 and the next theorem bj-elpwgALT 37487 are alternate proofs of velpw 4554 and elpwg 4552 respectively, where one proves first the setvar case and then generalizes using vtoclbg 3518 instead of proving first the general case using elab2g 3634 and then specifying. Here, this results in needing an extra DV condition, a longer combined proof and use of ax-12 2206. In other cases, that order is better (e.g., vsnex 5386 proved before snexg 5391). (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 4551	. . 3 ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴}
2	1	eleq2i 2848	. 2 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ∈ {𝑥 ∣ 𝑥 ⊆ 𝐴})
3		abid 2738	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝑥 ⊆ 𝐴} ↔ 𝑥 ⊆ 𝐴)
4	2, 3	bitri 277	1 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)

Syntax hints:   ↔ wb 208   ∈ wcel 2136  {cab 2734   ⊆ wss 3899  𝒫 cpw 4549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-12 2206  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-pw 4551

This theorem is referenced by:  bj-elpwgALT  37487