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 V B W C A B C = A C = A B

Proof

Step Hyp Ref Expression
1 dfopg A V B W A B = A A B
2 eleq2 A B = A A B C A B C A A B
3 snex A V
4 prex A B V
5 3 4 elpr2 C A A B C = A C = A B
6 2 5 bitrdi A B = A A B C A B C = A C = A B
7 1 6 syl A V B W C A B C = A C = A B