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 C_ { x e. V | ph } <-> V = { x e. V | ph } )

Proof

Step	Hyp	Ref	Expression
1		ssrab2	|- { x e. V | ph } C_ V
2	1	biantru	|- ( V C_ { x e. V | ph } <-> ( V C_ { x e. V | ph } /\ { x e. V | ph } C_ V ) )
3		eqss	|- ( V = { x e. V | ph } <-> ( V C_ { x e. V | ph } /\ { x e. V | ph } C_ V ) )
4	2 3	bitr4i	|- ( V C_ { x e. V | ph } <-> V = { x e. V | ph } )