Metamath Proof Explorer

Theorem opnzi

Description: An ordered pair is nonempty if the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypotheses opth1.1 
|- A e. _V
opth1.2 
|- B e. _V
Assertion opnzi 
|- <. A , B >. =/= (/)

Proof

Step Hyp Ref Expression
1 opth1.1 
 |-  A e. _V
2 opth1.2 
 |-  B e. _V
3 opnz 
 |-  ( <. A , B >. =/= (/) <-> ( A e. _V /\ B e. _V ) )
4 1 2 3 mpbir2an 
 |-  <. A , B >. =/= (/)