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

Proof

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