Metamath Proof Explorer

Theorem compab

Description: Two ways of saying "the complement of a class abstraction". (Contributed by Andrew Salmon, 15-Jul-2011) (Proof shortened by Mario Carneiro, 11-Dec-2016)

Ref Expression
Assertion compab 
|- ( _V \ { z | ph } ) = { z | -. ph }

Proof

Step Hyp Ref Expression
1 nfcv 
 |-  F/_ z _V
2 nfab1 
 |-  F/_ z { z | ph }
3 1 2 nfdif 
 |-  F/_ z ( _V \ { z | ph } )
4 nfab1 
 |-  F/_ z { z | -. ph }
5 3 4 cleqf 
 |-  ( ( _V \ { z | ph } ) = { z | -. ph } <-> A. z ( z e. ( _V \ { z | ph } ) <-> z e. { z | -. ph } ) )
6 abid 
 |-  ( z e. { z | ph } <-> ph )
7 6 notbii 
 |-  ( -. z e. { z | ph } <-> -. ph )
8 velcomp 
 |-  ( z e. ( _V \ { z | ph } ) <-> -. z e. { z | ph } )
9 abid 
 |-  ( z e. { z | -. ph } <-> -. ph )
10 7 8 9 3bitr4i 
 |-  ( z e. ( _V \ { z | ph } ) <-> z e. { z | -. ph } )
11 5 10 mpgbir 
 |-  ( _V \ { z | ph } ) = { z | -. ph }