Theorem difrab0eq

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

	Ref	Expression
Assertion	difrab0eq	|- ( ( V \ { x e. V | ph } ) = (/) <-> V = { x e. V | ph } )

Proof

Step	Hyp	Ref	Expression
1		ssdif0	|- ( V C_ { x e. V | ph } <-> ( V \ { x e. V | ph } ) = (/) )
2		ssrabeq	|- ( V C_ { x e. V | ph } <-> V = { x e. V | ph } )
3	1 2	bitr3i	|- ( ( V \ { x e. V | ph } ) = (/) <-> V = { x e. V | ph } )