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 )