Theorem notab

Description: A class abstraction defined by a negation. (Contributed by FL, 18-Sep-2010)

	Ref	Expression
Assertion	notab	|- { x | -. ph } = ( _V \ { x | ph } )

Proof

Step	Hyp	Ref	Expression
1		df-rab	|- { x e. _V | -. ph } = { x | ( x e. _V /\ -. ph ) }
2		rabab	|- { x e. _V | -. ph } = { x | -. ph }
3	1 2	eqtr3i	|- { x | ( x e. _V /\ -. ph ) } = { x | -. ph }
4		difab	|- ( { x | x e. _V } \ { x | ph } ) = { x | ( x e. _V /\ -. ph ) }
5		abid2	|- { x | x e. _V } = _V
6	5	difeq1i	|- ( { x | x e. _V } \ { x | ph } ) = ( _V \ { x | ph } )
7	4 6	eqtr3i	|- { x | ( x e. _V /\ -. ph ) } = ( _V \ { x | ph } )
8	3 7	eqtr3i	|- { x | -. ph } = ( _V \ { x | ph } )