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

Metamath Proof Explorer

Theorem vvdifopab

Description: Ordered-pair class abstraction defined by a negation. (Contributed by Peter Mazsa, 25-Jun-2019)

Ref Expression
Assertion vvdifopab 
|- ( ( _V X. _V ) \ { <. x , y >. | ph } ) = { <. x , y >. | -. ph }

Proof

Step Hyp Ref Expression
1 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
2 1 notbii 
 |-  ( -. <. x , y >. e. { <. x , y >. | ph } <-> -. ph )
3 opelvvdif 
 |-  ( ( x e. _V /\ y e. _V ) -> ( <. x , y >. e. ( ( _V X. _V ) \ { <. x , y >. | ph } ) <-> -. <. x , y >. e. { <. x , y >. | ph } ) )
4 3 el2v 
 |-  ( <. x , y >. e. ( ( _V X. _V ) \ { <. x , y >. | ph } ) <-> -. <. x , y >. e. { <. x , y >. | ph } )
5 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | -. ph } <-> -. ph )
6 2 4 5 3bitr4i 
 |-  ( <. x , y >. e. ( ( _V X. _V ) \ { <. x , y >. | ph } ) <-> <. x , y >. e. { <. x , y >. | -. ph } )
7 6 gen2 
 |-  A. x A. y ( <. x , y >. e. ( ( _V X. _V ) \ { <. x , y >. | ph } ) <-> <. x , y >. e. { <. x , y >. | -. ph } )
8 relxp 
 |-  Rel ( _V X. _V )
9 reldif 
 |-  ( Rel ( _V X. _V ) -> Rel ( ( _V X. _V ) \ { <. x , y >. | ph } ) )
10 8 9 ax-mp 
 |-  Rel ( ( _V X. _V ) \ { <. x , y >. | ph } )
11 relopabv 
 |-  Rel { <. x , y >. | -. ph }
12 nfcv 
 |-  F/_ x ( _V X. _V )
13 nfopab1 
 |-  F/_ x { <. x , y >. | ph }
14 12 13 nfdif 
 |-  F/_ x ( ( _V X. _V ) \ { <. x , y >. | ph } )
15 nfopab1 
 |-  F/_ x { <. x , y >. | -. ph }
16 nfcv 
 |-  F/_ y ( _V X. _V )
17 nfopab2 
 |-  F/_ y { <. x , y >. | ph }
18 16 17 nfdif 
 |-  F/_ y ( ( _V X. _V ) \ { <. x , y >. | ph } )
19 nfopab2 
 |-  F/_ y { <. x , y >. | -. ph }
20 14 15 18 19 eqrelf 
 |-  ( ( Rel ( ( _V X. _V ) \ { <. x , y >. | ph } ) /\ Rel { <. x , y >. | -. ph } ) -> ( ( ( _V X. _V ) \ { <. x , y >. | ph } ) = { <. x , y >. | -. ph } <-> A. x A. y ( <. x , y >. e. ( ( _V X. _V ) \ { <. x , y >. | ph } ) <-> <. x , y >. e. { <. x , y >. | -. ph } ) ) )
21 10 11 20 mp2an 
 |-  ( ( ( _V X. _V ) \ { <. x , y >. | ph } ) = { <. x , y >. | -. ph } <-> A. x A. y ( <. x , y >. e. ( ( _V X. _V ) \ { <. x , y >. | ph } ) <-> <. x , y >. e. { <. x , y >. | -. ph } ) )
22 7 21 mpbir 
 |-  ( ( _V X. _V ) \ { <. x , y >. | ph } ) = { <. x , y >. | -. ph }