Theorem bj-velpwALT 36424

Description: This theorem bj-velpwALT 36424 and the next theorem bj-elpwgALT 36425 are alternate proofs of velpw 4599 and elpwg 4597 respectively, where one proves first the setvar case and then generalizes using vtoclbg 3537 instead of proving first the general case using elab2g 3662 and then specifying. Here, this results in needing an extra DV condition, a longer combined proof and use of ax-12 2163. In other cases, that order is better (e.g., vsnex 5419 proved before snexg 5420). (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 4596	. . 3 ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴}
2	1	eleq2i 2817	. 2 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ∈ {𝑥 ∣ 𝑥 ⊆ 𝐴})
3		abid 2705	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝑥 ⊆ 𝐴} ↔ 𝑥 ⊆ 𝐴)
4	2, 3	bitri 275	1 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)

Syntax hints:   ↔ wb 205   ∈ wcel 2098  {cab 2701   ⊆ wss 3940  𝒫 cpw 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-12 2163  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-pw 4596

This theorem is referenced by:  bj-elpwgALT  36425