Metamath Proof Explorer

Theorem oprcl

Description: If an ordered pair has an element, then its arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 n0i 
 |-  ( C e. <. A , B >. -> -. <. A , B >. = (/) )
2 opprc 
 |-  ( -. ( A e. _V /\ B e. _V ) -> <. A , B >. = (/) )
3 1 2 nsyl2 
 |-  ( C e. <. A , B >. -> ( A e. _V /\ B e. _V ) )