Metamath Proof Explorer

Theorem elpr2

Description: A member of a pair of sets is one or the other of them, and conversely. Exercise 1 of TakeutiZaring p. 15. (Contributed by NM, 14-Oct-2005) (Proof shortened by JJ, 23-Jul-2021)

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


Step Hyp Ref Expression
1 elpr2.1 B V
2 elpr2.2 C V
3 elpr2g B V C V A B C A = B A = C
4 1 2 3 mp2an A B C A = B A = C