Theorem opeq2d 4409

Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)

Hypothesis

Ref	Expression
opeq1d.1	|- ( ph -> A = B )

Assertion

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

Proof of Theorem opeq2d

Step	Hyp	Ref	Expression
1		opeq1d.1	. 2 |- ( ph -> A = B )
2		opeq2 4403	. 2 |- ( A = B -> <. C , A >. = <. C , B >. )
3	1, 2	syl 17	1 |- ( ph -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   = wceq 1483   <.cop 4183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184

This theorem is referenced by:  funopsn  6413  fmptsng  6434  fmptsnd  6435  tfrlem11  7484  seqomlem0  7544  seqomlem1  7545  seqomlem4  7548  seqomeq12  7549  fundmen  8030  unxpdomlem1  8164  mulcanenq  9782  elreal2  9953  om2uzrdg  12755  uzrdgsuci  12759  seqeq2  12805  seqeq3  12806  s1val  13378  s1eq  13380  swrdlsw  13452  swrdccatwrd  13468  ccats1swrdeq  13469  ccatopth  13470  swrdccat  13493  swrdccat3blem  13495  swrdccat3b  13496  swrdccatin12d  13501  splval  13502  splcl  13503  cshfn  13536  cshw0  13540  cshwmodn  13541  repswcshw  13558  swrds2  13685  swrd2lsw  13695  eucalgval  15295  setsidvald  15889  ressval  15927  ressress  15938  prdsval  16115  imasval  16171  imasaddvallem  16189  cidval  16338  iscatd2  16342  oppcval  16373  ismon  16393  rescval  16487  idfucl  16541  funcres  16556  fucval  16618  fucpropd  16637  setcval  16727  catcval  16746  estrcval  16764  xpcval  16817  1stfcl  16837  2ndfcl  16838  curf12  16867  curf2val  16870  curfcl  16872  hofcl  16899  oduval  17130  ipoval  17154  frmdval  17388  oppgval  17777  symgval  17799  efgmval  18125  efgmnvl  18127  efgi  18132  frgpup3lem  18190  dprd2da  18441  dmdprdpr  18448  dprdpr  18449  pgpfaclem1  18480  mgpval  18492  mgpress  18500  opprval  18624  sraval  19176  rlmval2  19194  psrval  19362  opsrval  19474  opsrval2  19476  zlmval  19864  znval  19883  znval2  19885  thlval  20039  islindf4  20177  matval  20217  mat1dimmul  20282  mat1dimcrng  20283  mat1scmat  20345  mdet0pr  20398  m1detdiag  20403  txkgen  21455  pt1hmeo  21609  xpstopnlem1  21612  tusval  22070  tmsval  22286  tngval  22443  om1val  22830  pi1xfrcnvlem  22856  pi1xfrcnv  22857  dchrval  24959  ttgval  25755  eengv  25859  uspgr1ewop  26140  usgr2v1e2w  26144  1loopgruspgr  26396  1egrvtxdg1r  26406  1egrvtxdg0  26407  wwlksnextwrd  26792  wwlksnextproplem3  26806  clwlkclwwlk2  26904  clwwlksf1  26917  clwlksfoclwwlk  26963  clwlksf1clwwlklem  26968  clwlksf1clwwlk  26969  clwlkssizeeq  26971  eupth2lem3lem3  27090  eupth2  27099  numclwlk1lem2f1  27227  numclwlk2lem2f1o  27238  br8d  29422  resvval  29827  smatfval  29861  smatrcl  29862  smatlem  29863  fvproj  29899  qqhval  30018  iwrdsplit  30449  bnj66  30930  bnj1234  31081  bnj1296  31089  bnj1450  31118  bnj1463  31123  bnj1501  31135  bnj1523  31139  subfacp1lem5  31166  cvmliftlem10  31276  cvmlift2lem12  31296  msubffval  31420  msubfval  31421  elmsubrn  31425  msubrn  31426  msubco  31428  br8  31646  br6  31647  nosupbnd2lem1  31861  btwnouttr2  32129  brfs  32186  btwnconn1lem11  32204  csbfinxpg  33225  finixpnum  33394  ldualset  34412  tgrpfset  36032  tgrpset  36033  erngfset  36087  erngset  36088  erngfset-rN  36095  erngset-rN  36096  dvafset  36292  dvaset  36293  dvhfset  36369  dvhset  36370  dvhfvadd  36380  dvhopvadd2  36383  dib1dim2  36457  dicvscacl  36480  cdlemn6  36491  dihopelvalcpre  36537  dih1dimatlem  36618  hdmapfval  37119  hlhilset  37226  mendval  37753  ovolval4lem1  40863  ovolval4lem2  40864  ovnovollem3  40872  pfxpfx  41415  pfxccatin12d  41432  idfusubc0  41865  idfusubc  41866  rngcvalALTV  41961  ringcvalALTV  42007  zlmodzxzsub  42138  lmod1zr  42282