Metamath Proof Explorer

Theorem 0nelopabOLD

Description: Obsolete version of 0nelopab as of 3-Oct-2024. (Contributed by Alexander van der Vekens, 5-Nov-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 0nelopabOLD 
|- -. (/) e. { <. x , y >. | ph }

Proof

Step Hyp Ref Expression
1 elopab 
 |-  ( (/) e. { <. x , y >. | ph } <-> E. x E. y ( (/) = <. x , y >. /\ ph ) )
2 nfopab1 
 |-  F/_ x { <. x , y >. | ph }
3 2 nfel2 
 |-  F/ x (/) e. { <. x , y >. | ph }
4 3 nfn 
 |-  F/ x -. (/) e. { <. x , y >. | ph }
5 nfopab2 
 |-  F/_ y { <. x , y >. | ph }
6 5 nfel2 
 |-  F/ y (/) e. { <. x , y >. | ph }
7 6 nfn 
 |-  F/ y -. (/) e. { <. x , y >. | ph }
8 vex 
 |-  x e. _V
9 vex 
 |-  y e. _V
10 8 9 opnzi 
 |-  <. x , y >. =/= (/)
11 nesym 
 |-  ( <. x , y >. =/= (/) <-> -. (/) = <. x , y >. )
12 pm2.21 
 |-  ( -. (/) = <. x , y >. -> ( (/) = <. x , y >. -> -. (/) e. { <. x , y >. | ph } ) )
13 11 12 sylbi 
 |-  ( <. x , y >. =/= (/) -> ( (/) = <. x , y >. -> -. (/) e. { <. x , y >. | ph } ) )
14 10 13 ax-mp 
 |-  ( (/) = <. x , y >. -> -. (/) e. { <. x , y >. | ph } )
15 14 adantr 
 |-  ( ( (/) = <. x , y >. /\ ph ) -> -. (/) e. { <. x , y >. | ph } )
16 7 15 exlimi 
 |-  ( E. y ( (/) = <. x , y >. /\ ph ) -> -. (/) e. { <. x , y >. | ph } )
17 4 16 exlimi 
 |-  ( E. x E. y ( (/) = <. x , y >. /\ ph ) -> -. (/) e. { <. x , y >. | ph } )
18 1 17 sylbi 
 |-  ( (/) e. { <. x , y >. | ph } -> -. (/) e. { <. x , y >. | ph } )
19 id 
 |-  ( -. (/) e. { <. x , y >. | ph } -> -. (/) e. { <. x , y >. | ph } )
20 18 19 pm2.61i 
 |-  -. (/) e. { <. x , y >. | ph }