Theorem bj-velpwALT 37034

Description: This theorem bj-velpwALT 37034 and the next theorem bj-elpwgALT 37035 are alternate proofs of velpw 4564 and elpwg 4562 respectively, where one proves first the setvar case and then generalizes using vtoclbg 3520 instead of proving first the general case using elab2g 3644 and then specifying. Here, this results in needing an extra DV condition, a longer combined proof and use of ax-12 2178. In other cases, that order is better (e.g., vsnex 5384 proved before snexg 5385). (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 4561	. . 3 ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴}
2	1	eleq2i 2820	. 2 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ∈ {𝑥 ∣ 𝑥 ⊆ 𝐴})
3		abid 2711	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝑥 ⊆ 𝐴} ↔ 𝑥 ⊆ 𝐴)
4	2, 3	bitri 275	1 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)

Syntax hints:   ↔ wb 206   ∈ wcel 2109  {cab 2707   ⊆ wss 3911  𝒫 cpw 4559

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 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-pw 4561

This theorem is referenced by:  bj-elpwgALT  37035