Metamath Proof Explorer

Theorem opeq1

Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ A = B → A ∈ V ↔ B ∈ V
2 1 anbi1d ⊢ A = B → A ∈ V ∧ C ∈ V ↔ B ∈ V ∧ C ∈ V
3 sneq ⊢ A = B → A = B
4 preq1 ⊢ A = B → A C = B C
5 3 4 preq12d ⊢ A = B → A A C = B B C
6 2 5 ifbieq1d ⊢ A = B → if A ∈ V ∧ C ∈ V A A C ∅ = if B ∈ V ∧ C ∈ V B B C ∅
7 dfopif ⊢ A C = if A ∈ V ∧ C ∈ V A A C ∅
8 dfopif ⊢ B C = if B ∈ V ∧ C ∈ V B B C ∅
9 6 7 8 3eqtr4g ⊢ A = B → A C = B C