Metamath Proof Explorer


Theorem elprg

Description: A member of a pair of classes is one or the other of them, and conversely as soon as it is a set. Exercise 1 of TakeutiZaring p. 15, generalized. (Contributed by NM, 13-Sep-1995)

Ref Expression
Assertion elprg A V A B C A = B A = C

Proof

Step Hyp Ref Expression
1 eqeq1 x = A x = B A = B
2 eqeq1 x = A x = C A = C
3 1 2 orbi12d x = A x = B x = C A = B A = C
4 dfpr2 B C = x | x = B x = C
5 3 4 elab2g A V A B C A = B A = C