Metamath Proof Explorer

Theorem elop

Description: Characterization of the elements of an ordered pair. Exercise 3 of TakeutiZaring p. 15. (Contributed by NM, 15-Jul-1993) (Revised by Mario Carneiro, 26-Apr-2015) Remove an extraneous hypothesis. (Revised by BJ, 25-Dec-2020) (Avoid depending on this detail.)

Ref Expression
Hypotheses elop.1 B V
elop.2 C V
Assertion elop A B C A = B A = B C


Step Hyp Ref Expression
1 elop.1 B V
2 elop.2 C V
3 elopg B V C V A B C A = B A = B C
4 1 2 3 mp2an A B C A = B A = B C