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 }