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	⊢ 𝐵 ∈ V
	elpr2.2	⊢ 𝐶 ∈ V
Assertion	elpr2	⊢ ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		elpr2.1	⊢ 𝐵 ∈ V
2		elpr2.2	⊢ 𝐶 ∈ V
3		elpr2g	⊢ ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )
4	1 2 3	mp2an	⊢ ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) )