Metamath Proof Explorer


Theorem opnz

Description: An ordered pair is nonempty iff the arguments are sets. (Contributed by NM, 24-Jan-2004) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion opnz
|- ( <. A , B >. =/= (/) <-> ( A e. _V /\ B e. _V ) )

Proof

Step Hyp Ref Expression
1 opprc
 |-  ( -. ( A e. _V /\ B e. _V ) -> <. A , B >. = (/) )
2 1 necon1ai
 |-  ( <. A , B >. =/= (/) -> ( A e. _V /\ B e. _V ) )
3 dfopg
 |-  ( ( A e. _V /\ B e. _V ) -> <. A , B >. = { { A } , { A , B } } )
4 snex
 |-  { A } e. _V
5 4 prnz
 |-  { { A } , { A , B } } =/= (/)
6 5 a1i
 |-  ( ( A e. _V /\ B e. _V ) -> { { A } , { A , B } } =/= (/) )
7 3 6 eqnetrd
 |-  ( ( A e. _V /\ B e. _V ) -> <. A , B >. =/= (/) )
8 2 7 impbii
 |-  ( <. A , B >. =/= (/) <-> ( A e. _V /\ B e. _V ) )