Theorem ssextss

Description: An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004)

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

Proof

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