Metamath Proof Explorer

Theorem elpr2OLD

Description: Obsolete version of elpr2 as of 25-May-2024. (Contributed by NM, 14-Oct-2005) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses elpr2.1 ⊢B∈V
elpr2.2 ⊢C∈V
Assertion elpr2OLD ⊢A∈BC↔A=B∨A=C

Proof

Step Hyp Ref Expression
1 elpr2.1 ⊢B∈V
2 elpr2.2 ⊢C∈V
3 elex ⊢A∈BC→A∈V
4 eleq1 ⊢A=B→A∈V↔B∈V
5 1 4 mpbiri ⊢A=B→A∈V
6 eleq1 ⊢A=C→A∈V↔C∈V
7 2 6 mpbiri ⊢A=C→A∈V
8 5 7 jaoi ⊢A=B∨A=C→A∈V
9 elprg ⊢A∈V→A∈BC↔A=B∨A=C
10 3 8 9 pm5.21nii ⊢A∈BC↔A=B∨A=C