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∈BC↔A=B∨A=C

Proof

Step Hyp Ref Expression
1 elex ⊢A∈BC→A∈V
2 1 a1i ⊢B∈V∧C∈W→A∈BC→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∈BC↔A=B∨A=C
11 10 a1i ⊢B∈V∧C∈W→A∈V→A∈BC↔A=B∨A=C
12 2 9 11 pm5.21ndd ⊢B∈V∧C∈W→A∈BC↔A=B∨A=C