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

Metamath Proof Explorer

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 ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )