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 } ) ) )