# Metamath Proof Explorer

## Theorem opeq2

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 opeq2
`|- ( A = B -> <. C , A >. = <. C , B >. )`

### Proof

Step Hyp Ref Expression
1 eleq1
` |-  ( A = B -> ( A e. _V <-> B e. _V ) )`
2 preq2
` |-  ( A = B -> { C , A } = { C , B } )`
3 2 preq2d
` |-  ( A = B -> { { C } , { C , A } } = { { C } , { C , B } } )`
4 3 eleq2d
` |-  ( A = B -> ( x e. { { C } , { C , A } } <-> x e. { { C } , { C , B } } ) )`
5 1 4 3anbi23d
` |-  ( A = B -> ( ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) <-> ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) ) )`
6 5 abbidv
` |-  ( A = B -> { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) } = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) } )`
7 df-op
` |-  <. C , A >. = { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) }`
8 df-op
` |-  <. C , B >. = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) }`
9 6 7 8 3eqtr4g
` |-  ( A = B -> <. C , A >. = <. C , B >. )`