This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem notrab

Description: Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion notrab 
|- ( A \ { x e. A | ph } ) = { x e. A | -. ph }

Proof

Step Hyp Ref Expression
1 difab 
 |-  ( { x | x e. A } \ { x | ph } ) = { x | ( x e. A /\ -. ph ) }
2 difin 
 |-  ( A \ ( A i^i { x | ph } ) ) = ( A \ { x | ph } )
3 dfrab3 
 |-  { x e. A | ph } = ( A i^i { x | ph } )
4 3 difeq2i 
 |-  ( A \ { x e. A | ph } ) = ( A \ ( A i^i { x | ph } ) )
5 abid2 
 |-  { x | x e. A } = A
6 5 difeq1i 
 |-  ( { x | x e. A } \ { x | ph } ) = ( A \ { x | ph } )
7 2 4 6 3eqtr4i 
 |-  ( A \ { x e. A | ph } ) = ( { x | x e. A } \ { x | ph } )
8 df-rab 
 |-  { x e. A | -. ph } = { x | ( x e. A /\ -. ph ) }
9 1 7 8 3eqtr4i 
 |-  ( A \ { x e. A | ph } ) = { x e. A | -. ph }