This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opeq1

Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015)

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 1 anbi1d 
 |-  ( A = B -> ( ( A e. _V /\ C e. _V ) <-> ( B e. _V /\ C e. _V ) ) )
3 sneq 
 |-  ( A = B -> { A } = { B } )
4 preq1 
 |-  ( A = B -> { A , C } = { B , C } )
5 3 4 preq12d 
 |-  ( A = B -> { { A } , { A , C } } = { { B } , { B , C } } )
6 2 5 ifbieq1d 
 |-  ( A = B -> if ( ( A e. _V /\ C e. _V ) , { { A } , { A , C } } , (/) ) = if ( ( B e. _V /\ C e. _V ) , { { B } , { B , C } } , (/) ) )
7 dfopif 
 |-  <. A , C >. = if ( ( A e. _V /\ C e. _V ) , { { A } , { A , C } } , (/) )
8 dfopif 
 |-  <. B , C >. = if ( ( B e. _V /\ C e. _V ) , { { B } , { B , C } } , (/) )
9 6 7 8 3eqtr4g 
 |-  ( A = B -> <. A , C >. = <. B , C >. )