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

Proof

Step Hyp Ref Expression
1 elpr2.1 ⊢ B ∈ V
2 elpr2.2 ⊢ C ∈ V
3 elex ⊢ A ∈ B C → 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 ∈ B C ↔ A = B ∨ A = C
10 3 8 9 pm5.21nii ⊢ A ∈ B C ↔ A = B ∨ A = C