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∈BC↔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∈BC↔A=B∨A=C
4 1 2 3 mp2an ⊢A∈BC↔A=B∨A=C