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∈BC→A=B∨A=C

Proof

Step Hyp Ref Expression
1 elprg ⊢A∈BC→A∈BC↔A=B∨A=C
2 1 ibi ⊢A∈BC→A=B∨A=C