Theorem pwss

Description: Subclass relationship for power class. (Contributed by NM, 21-Jun-2009)

	Ref	Expression
Assertion	pwss	$$⊢𝒫A\subseteq B\leftrightarrow \forall x\left(x\subseteq A\to x\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ss	$$⊢𝒫A\subseteq B\leftrightarrow \forall x\left(x\in 𝒫A\to x\in B\right)$$
2		velpw	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$
3	2	imbi1i	$$⊢\left(x\in 𝒫A\to x\in B\right)\leftrightarrow \left(x\subseteq A\to x\in B\right)$$
4	3	albii	$$⊢\forall x\left(x\in 𝒫A\to x\in B\right)\leftrightarrow \forall x\left(x\subseteq A\to x\in B\right)$$
5	1 4	bitri	$$⊢𝒫A\subseteq B\leftrightarrow \forall x\left(x\subseteq A\to x\in B\right)$$