Theorem bj-velpwALT

Description: This theorem bj-velpwALT and the next theorem bj-elpwgALT are alternate proofs of velpw and elpwg respectively, where one proves first the setvar case and then generalizes using vtoclbg instead of proving first the general case using elab2g and then specifying. Here, this results in needing an extra DV condition, a longer combined proof and use of ax-12 . In other cases, that order is better (e.g., vsnex proved before snexg ). (Contributed by BJ, 17-Jan-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-velpwALT	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		df-pw	$$⊢𝒫A=\left\{x|x\subseteq A\right\}$$
2	1	eleq2i	$$⊢x\in 𝒫A\leftrightarrow x\in \left\{x|x\subseteq A\right\}$$
3		abid	$$⊢x\in \left\{x|x\subseteq A\right\}\leftrightarrow x\subseteq A$$
4	2 3	bitri	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$