Metamath Proof Explorer

Theorem opeq2OLD

Description: Obsolete version of opeq2 as of 25-May-2024. (Contributed by NM, 25-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion opeq2OLD ⊢ A = B → C A = C B

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ A = B → A ∈ V ↔ B ∈ V
2 1 anbi2d ⊢ A = B → C ∈ V ∧ A ∈ V ↔ C ∈ V ∧ B ∈ V
3 preq2 ⊢ A = B → C A = C B
4 3 preq2d ⊢ A = B → C C A = C C B
5 2 4 ifbieq1d ⊢ A = B → if C ∈ V ∧ A ∈ V C C A ∅ = if C ∈ V ∧ B ∈ V C C B ∅
6 dfopif ⊢ C A = if C ∈ V ∧ A ∈ V C C A ∅
7 dfopif ⊢ C B = if C ∈ V ∧ B ∈ V C C B ∅
8 5 6 7 3eqtr4g ⊢ A = B → C A = C B