Theorem elpwbi

Description: Membership in a power set, biconditional. (Contributed by Steven Nguyen, 17-Jul-2022) (Proof shortened by Steven Nguyen, 16-Sep-2022)

	Ref	Expression
Hypothesis	elpwbi.1	$$⊢B\in \mathrm{V}$$
Assertion	elpwbi	$$⊢A\subseteq B\leftrightarrow A\in 𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		elpwbi.1	$$⊢B\in \mathrm{V}$$
2	1	elpw2	$$⊢A\in 𝒫B\leftrightarrow A\subseteq B$$
3	2	bicomi	$$⊢A\subseteq B\leftrightarrow A\in 𝒫B$$