This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elopg

Description: Characterization of the elements of an ordered pair. Closed form of elop . (Contributed by BJ, 22-Jun-2019) (Avoid depending on this detail.)

Ref Expression
Assertion elopg 
|- ( ( A e. V /\ B e. W ) -> ( C e. <. A , B >. <-> ( C = { A } \/ C = { A , B } ) ) )

Proof

Step Hyp Ref Expression
1 dfopg 
 |-  ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2 eleq2 
 |-  ( <. A , B >. = { { A } , { A , B } } -> ( C e. <. A , B >. <-> C e. { { A } , { A , B } } ) )
3 snex 
 |-  { A } e. _V
4 prex 
 |-  { A , B } e. _V
5 3 4 elpr2 
 |-  ( C e. { { A } , { A , B } } <-> ( C = { A } \/ C = { A , B } ) )
6 2 5 bitrdi 
 |-  ( <. A , B >. = { { A } , { A , B } } -> ( C e. <. A , B >. <-> ( C = { A } \/ C = { A , B } ) ) )
7 1 6 syl 
 |-  ( ( A e. V /\ B e. W ) -> ( C e. <. A , B >. <-> ( C = { A } \/ C = { A , B } ) ) )