Theorem elpw2g

Description: Membership in a power class. Theorem 86 of Suppes p. 47. (Contributed by NM, 7-Aug-2000)

	Ref	Expression
Assertion	elpw2g	$$⊢B\in V\to \left(A\in 𝒫B\leftrightarrow A\subseteq B\right)$$

Proof

Step	Hyp	Ref	Expression
1		elpwi	$$⊢A\in 𝒫B\to A\subseteq B$$
2		ssexg	$$⊢\left(A\subseteq B\wedge B\in V\right)\to A\in \mathrm{V}$$
3		elpwg	$$⊢A\in \mathrm{V}\to \left(A\in 𝒫B\leftrightarrow A\subseteq B\right)$$
4	3	biimparc	$$⊢\left(A\subseteq B\wedge A\in \mathrm{V}\right)\to A\in 𝒫B$$
5	2 4	syldan	$$⊢\left(A\subseteq B\wedge B\in V\right)\to A\in 𝒫B$$
6	5	expcom	$$⊢B\in V\to \left(A\subseteq B\to A\in 𝒫B\right)$$
7	1 6	impbid2	$$⊢B\in V\to \left(A\in 𝒫B\leftrightarrow A\subseteq B\right)$$