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 ⊢ B ∈ V ∧ C ∈ W → A ∈ B C ↔ A = B ∨ A = C

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ B C → A ∈ V
2 1 a1i ⊢ B ∈ V ∧ C ∈ W → A ∈ B C → A ∈ V
3 elex ⊢ B ∈ V → B ∈ V
4 eleq1a ⊢ B ∈ V → A = B → A ∈ V
5 3 4 syl ⊢ B ∈ V → A = B → A ∈ V
6 elex ⊢ C ∈ W → C ∈ V
7 eleq1a ⊢ C ∈ V → A = C → A ∈ V
8 6 7 syl ⊢ C ∈ W → A = C → A ∈ V
9 5 8 jaao ⊢ B ∈ V ∧ C ∈ W → A = B ∨ A = C → A ∈ V
10 elprg ⊢ A ∈ V → A ∈ B C ↔ A = B ∨ A = C
11 10 a1i ⊢ B ∈ V ∧ C ∈ W → A ∈ V → A ∈ B C ↔ A = B ∨ A = C
12 2 9 11 pm5.21ndd ⊢ B ∈ V ∧ C ∈ W → A ∈ B C ↔ A = B ∨ A = C