Theorem ssrabeq

Description: If the restricting class of a restricted class abstraction is a subset of this restricted class abstraction, it is equal to this restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017)

	Ref	Expression
Assertion	ssrabeq	$$⊢V\subseteq \left\{x\in V|\phi \right\}\leftrightarrow V=\left\{x\in V|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		ssrab2	$$⊢\left\{x\in V|\phi \right\}\subseteq V$$
2	1	biantru	$$⊢V\subseteq \left\{x\in V|\phi \right\}\leftrightarrow \left(V\subseteq \left\{x\in V|\phi \right\}\wedge \left\{x\in V|\phi \right\}\subseteq V\right)$$
3		eqss	$$⊢V=\left\{x\in V|\phi \right\}\leftrightarrow \left(V\subseteq \left\{x\in V|\phi \right\}\wedge \left\{x\in V|\phi \right\}\subseteq V\right)$$
4	2 3	bitr4i	$$⊢V\subseteq \left\{x\in V|\phi \right\}\leftrightarrow V=\left\{x\in V|\phi \right\}$$