Metamath Proof Explorer

Theorem opeq1

Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015) Avoid ax-10 , ax-11 , ax-12 . (Revised by Gino Giotto, 26-May-2024)

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

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ A = B → A ∈ V ↔ B ∈ V
2 sneq ⊢ A = B → A = B
3 preq1 ⊢ A = B → A C = B C
4 2 3 preq12d ⊢ A = B → A A C = B B C
5 4 eleq2d ⊢ A = B → x ∈ A A C ↔ x ∈ B B C
6 1 5 3anbi13d ⊢ A = B → A ∈ V ∧ C ∈ V ∧ x ∈ A A C ↔ B ∈ V ∧ C ∈ V ∧ x ∈ B B C
7 6 abbidv ⊢ A = B → x | A ∈ V ∧ C ∈ V ∧ x ∈ A A C = x | B ∈ V ∧ C ∈ V ∧ x ∈ B B C
8 df-op ⊢ A C = x | A ∈ V ∧ C ∈ V ∧ x ∈ A A C
9 df-op ⊢ B C = x | B ∈ V ∧ C ∈ V ∧ x ∈ B B C
10 7 8 9 3eqtr4g ⊢ A = B → A C = B C