This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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