Theorem ss2ab

Description: Class abstractions in a subclass relationship. (Contributed by NM, 3-Jul-1994)

	Ref	Expression
Assertion	ss2ab	$$⊢\left\{x|\phi \right\}\subseteq \left\{x|\psi \right\}\leftrightarrow \forall x\left(\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfab1	$$⊢\underset{\_}{Ⅎ}x\left\{x|\phi \right\}$$
2		nfab1	$$⊢\underset{\_}{Ⅎ}x\left\{x|\psi \right\}$$
3	1 2	dfss2f	$$⊢\left\{x|\phi \right\}\subseteq \left\{x|\psi \right\}\leftrightarrow \forall x\left(x\in \left\{x|\phi \right\}\to x\in \left\{x|\psi \right\}\right)$$
4		abid	$$⊢x\in \left\{x|\phi \right\}\leftrightarrow \phi$$
5		abid	$$⊢x\in \left\{x|\psi \right\}\leftrightarrow \psi$$
6	4 5	imbi12i	$$⊢\left(x\in \left\{x|\phi \right\}\to x\in \left\{x|\psi \right\}\right)\leftrightarrow \left(\phi \to \psi \right)$$
7	6	albii	$$⊢\forall x\left(x\in \left\{x|\phi \right\}\to x\in \left\{x|\psi \right\}\right)\leftrightarrow \forall x\left(\phi \to \psi \right)$$
8	3 7	bitri	$$⊢\left\{x|\phi \right\}\subseteq \left\{x|\psi \right\}\leftrightarrow \forall x\left(\phi \to \psi \right)$$