Metamath Proof Explorer

Theorem elpri

Description: If a class is an element of a pair, then it is one of the two paired elements. (Contributed by Scott Fenton, 1-Apr-2011)

Ref Expression
Assertion elpri A B C A = B A = C


Step Hyp Ref Expression
1 elprg A B C A B C A = B A = C
2 1 ibi A B C A = B A = C