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 >. )