Theorem elpr2g

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) Generalize from sethood hypothesis to sethood antecedent. (Revised by BJ, 25-May-2024)

	Ref	Expression
Assertion	elpr2g	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ { 𝐵 , 𝐶 } → 𝐴 ∈ V )
2	1	a1i	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐴 ∈ { 𝐵 , 𝐶 } → 𝐴 ∈ V ) )
3		elex	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ V )
4		eleq1a	⊢ ( 𝐵 ∈ V → ( 𝐴 = 𝐵 → 𝐴 ∈ V ) )
5	3 4	syl	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 = 𝐵 → 𝐴 ∈ V ) )
6		elex	⊢ ( 𝐶 ∈ 𝑊 → 𝐶 ∈ V )
7		eleq1a	⊢ ( 𝐶 ∈ V → ( 𝐴 = 𝐶 → 𝐴 ∈ V ) )
8	6 7	syl	⊢ ( 𝐶 ∈ 𝑊 → ( 𝐴 = 𝐶 → 𝐴 ∈ V ) )
9	5 8	jaao	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) → 𝐴 ∈ V ) )
10		elprg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )
11	10	a1i	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐴 ∈ V → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) ) )
12	2 9 11	pm5.21ndd	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )