Theorem opeq1 3819

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

Assertion

Ref	Expression
opeq1	|- ( A = B -> <. A , C >. = <. B , C >. )

Proof of Theorem opeq1

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2268	. . . . . 6 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi1d 465	. . . . 5 |- ( A = B -> ( ( A e. _V /\ C e. _V ) <-> ( B e. _V /\ C e. _V ) ) )
3		sneq 3644	. . . . . . 7 |- ( A = B -> { A } = { B } )
4		preq1 3710	. . . . . . 7 |- ( A = B -> { A , C } = { B , C } )
5	3, 4	preq12d 3718	. . . . . 6 |- ( A = B -> { { A } , { A , C } } = { { B } , { B , C } } )
6	5	eleq2d 2275	. . . . 5 |- ( A = B -> ( x e. { { A } , { A , C } } <-> x e. { { B } , { B , C } } ) )
7	2, 6	anbi12d 473	. . . 4 |- ( A = B -> ( ( ( A e. _V /\ C e. _V ) /\ x e. { { A } , { A , C } } ) <-> ( ( B e. _V /\ C e. _V ) /\ x e. { { B } , { B , C } } ) ) )
8		df-3an 983	. . . 4 |- ( ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) <-> ( ( A e. _V /\ C e. _V ) /\ x e. { { A } , { A , C } } ) )
9		df-3an 983	. . . 4 |- ( ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) <-> ( ( B e. _V /\ C e. _V ) /\ x e. { { B } , { B , C } } ) )
10	7, 8, 9	3bitr4g 223	. . 3 |- ( A = B -> ( ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) <-> ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) ) )
11	10	abbidv 2323	. 2 |- ( 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 } } ) } )
12		df-op 3642	. 2 |- <. A , C >. = { x | ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) }
13		df-op 3642	. 2 |- <. B , C >. = { x | ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) }
14	11, 12, 13	3eqtr4g 2263	1 |- ( A = B -> <. A , C >. = <. B , C >. )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 981   = wceq 1373   e. wcel 2176   {cab 2191   _Vcvv 2772   {csn 3633   {cpr 3634   <.cop 3636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642

This theorem is referenced by:  opeq12  3821  opeq1i  3822  opeq1d  3825  oteq1  3828  breq1  4048  cbvopab1  4118  cbvopab1s  4120  opthg  4283  eqvinop  4288  opelopabsb  4307  opelxp  4706  elvvv  4739  opabid2  4810  opeliunxp2  4819  elsnres  4997  elimasng  5051  rnxpid  5118  dmsnopg  5155  cnvsng  5169  elxp4  5171  elxp5  5172  funopg  5306  f1osng  5565  dmfco  5649  fvelrn  5713  fsng  5755  fvsng  5782  funfvima3  5820  oveq1  5953  oprabid  5978  dfoprab2  5994  cbvoprab1  6019  opabex3d  6208  opabex3  6209  op1stg  6238  op2ndg  6239  oprssdmm  6259  dfoprab4f  6281  cnvoprab  6322  opeliunxp2f  6326  tfr1onlemaccex  6436  tfrcllemaccex  6449  elixpsn  6824  fundmen  6900  xpsnen  6918  xpassen  6927  xpf1o  6943  ltexnqq  7523  archnqq  7532  prarloclemarch2  7534  prarloclemlo  7609  prarloclem3  7612  prarloclem5  7615  caucvgprlemnkj  7781  caucvgprlemnbj  7782  caucvgprlemm  7783  caucvgprlemdisj  7789  caucvgprlemloc  7790  caucvgprlemcl  7791  caucvgprlemladdfu  7792  caucvgprlemladdrl  7793  caucvgprlem1  7794  caucvgprlem2  7795  caucvgpr  7797  caucvgprprlemell  7800  caucvgprprlemelu  7801  caucvgprprlemcbv  7802  caucvgprprlemval  7803  caucvgprprlemnkeqj  7805  caucvgprprlemmu  7810  caucvgprprlemopl  7812  caucvgprprlemlol  7813  caucvgprprlemopu  7814  caucvgprprlemloc  7818  caucvgprprlemclphr  7820  caucvgprprlemexbt  7821  caucvgprprlem1  7824  caucvgprprlem2  7825  caucvgsr  7917  suplocsrlemb  7921  suplocsrlempr  7922  suplocsrlem  7923  suplocsr  7924  elrealeu  7944  pitonn  7963  nntopi  8009  axcaucvglemval  8012  axcaucvg  8015  axpre-suploclemres  8016  fsum2dlemstep  11778  fprod2dlemstep  11966  imasaddfnlemg  13179  cnmpt21  14796