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