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 e. _V <-> B e. _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 e. { { A } , { A , C } } <-> x e. { { B } , { B , C } } ) )
6	1 5	3anbi13d	|- ( A = B -> ( ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) <-> ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) ) )
7	6	abbidv	|- ( A = B -> { x | ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) } = { x | ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) } )
8		df-op	|- <. A , C >. = { x | ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) }
9		df-op	|- <. B , C >. = { x | ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) }
10	7 8 9	3eqtr4g	|- ( A = B -> <. A , C >. = <. B , C >. )