Metamath Proof Explorer

Theorem opabn0

Description: Nonempty ordered pair class abstraction. (Contributed by NM, 10-Oct-2007)

Ref Expression
Assertion opabn0 
|- ( { <. x , y >. | ph } =/= (/) <-> E. x E. y ph )

Proof

Step Hyp Ref Expression
1 n0 
 |-  ( { <. x , y >. | ph } =/= (/) <-> E. z z e. { <. x , y >. | ph } )
2 elopab 
 |-  ( z e. { <. x , y >. | ph } <-> E. x E. y ( z = <. x , y >. /\ ph ) )
3 2 exbii 
 |-  ( E. z z e. { <. x , y >. | ph } <-> E. z E. x E. y ( z = <. x , y >. /\ ph ) )
4 exrot3 
 |-  ( E. z E. x E. y ( z = <. x , y >. /\ ph ) <-> E. x E. y E. z ( z = <. x , y >. /\ ph ) )
5 opex 
 |-  <. x , y >. e. _V
6 5 isseti 
 |-  E. z z = <. x , y >.
7 19.41v 
 |-  ( E. z ( z = <. x , y >. /\ ph ) <-> ( E. z z = <. x , y >. /\ ph ) )
8 6 7 mpbiran 
 |-  ( E. z ( z = <. x , y >. /\ ph ) <-> ph )
9 8 2exbii 
 |-  ( E. x E. y E. z ( z = <. x , y >. /\ ph ) <-> E. x E. y ph )
10 4 9 bitri 
 |-  ( E. z E. x E. y ( z = <. x , y >. /\ ph ) <-> E. x E. y ph )
11 3 10 bitri 
 |-  ( E. z z e. { <. x , y >. | ph } <-> E. x E. y ph )
12 1 11 bitri 
 |-  ( { <. x , y >. | ph } =/= (/) <-> E. x E. y ph )