Theorem opeq2d 4209

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 4203	. 2 |- ( A = B -> <. C , A >. = <. C , B >. )
3	1, 2	syl 16	1 |- ( ph -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   = wceq 1383   <.cop 4020

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021

This theorem is referenced by:  fmptsng  6077  fmptsnd  6078  tfrlem11  7059  seqomlem0  7116  seqomlem1  7117  seqomlem4  7120  seqomeq12  7121  fundmen  7591  unxpdomlem1  7726  mulcanenq  9341  elreal2  9512  om2uzrdg  12049  uzrdgsuci  12053  seqeq2  12093  seqeq3  12094  s1val  12592  s1eq  12594  swrdlsw  12659  swrdccatwrd  12675  ccats1swrdeq  12676  ccatopth  12677  wrdeqcats1  12681  swrdccat  12700  swrdccat3blem  12702  swrdccat3b  12703  swrdccatin12d  12708  splval  12709  splcl  12710  cshfn  12743  cshw0  12747  cshwmodn  12748  repswcshw  12762  swrds2  12865  swrd2lsw  12872  eucalgval  14193  ressval  14666  ressress  14676  prdsval  14834  imasval  14890  imasaddvallem  14908  cidval  15056  iscatd2  15060  oppcval  15090  ismon  15110  rescval  15178  idfucl  15229  funcres  15244  fucval  15306  fucpropd  15325  setcval  15383  catcval  15402  xpcval  15425  1stfcl  15445  2ndfcl  15446  curf12  15475  curf2val  15478  curfcl  15480  hofcl  15507  oduval  15739  ipoval  15763  frmdval  15998  oppgval  16361  symgval  16383  efgmval  16709  efgmnvl  16711  efgi  16716  frgpup3lem  16774  dprd2da  17070  dmdprdpr  17077  dprdpr  17078  pgpfaclem1  17111  mgpval  17123  mgpress  17131  opprval  17252  sraval  17801  rlmval2  17819  psrval  17990  opsrval  18118  opsrval2  18120  zlmval  18531  znval  18550  znval2  18554  thlval  18704  islindf4  18851  matval  18891  mat1dimmul  18956  mat1dimcrng  18957  mat1scmat  19019  mdet0pr  19072  m1detdiag  19077  txkgen  20131  pt1hmeo  20285  xpstopnlem1  20288  tusval  20747  tmsval  20962  tngval  21131  om1val  21508  pi1xfrcnvlem  21534  pi1xfrcnv  21535  dchrval  23487  ttgval  24156  eengv  24260  wwlkextwrd  24706  wwlkextproplem3  24721  clwlkisclwwlk2  24768  clwwlkf1  24774  clwlkfoclwwlk  24823  clwlkf1clwwlklem  24827  clwlkf1clwwlk  24828  clwlksizeeq  24830  eupath2lem3  24957  numclwlk1lem2f1  25072  numclwlk2lem2f1o  25083  br8d  27441  resvval  27795  fvproj  27813  qqhval  27933  iwrdsplit  28304  subfacp1lem5  28606  cvmliftlem10  28717  cvmlift2lem12  28737  msubffval  28861  msubfval  28862  elmsubrn  28866  msubrn  28867  msubco  28869  br8  29161  br6  29162  btwnouttr2  29648  brfs  29705  btwnconn1lem11  29723  finixpnum  30014  mendval  31108  setsidvald  32508  idfusubc0  32515  idfusubc  32516  estrcval  32596  rngcvalOLD  32644  ringcvalOLD  32687  zlmodzxzsub  32817  lmod1zr  32964  bnj66  33786  bnj1234  33937  bnj1296  33945  bnj1450  33974  bnj1463  33979  bnj1501  33991  bnj1523  33995  ldualset  34725  tgrpfset  36345  tgrpset  36346  erngfset  36400  erngset  36401  erngfset-rN  36408  erngset-rN  36409  dvafset  36605  dvaset  36606  dvhfset  36682  dvhset  36683  dvhfvadd  36693  dvhopvadd2  36696  dib1dim2  36770  dicvscacl  36793  cdlemn6  36804  dihopelvalcpre  36850  dih1dimatlem  36931  hdmapfval  37432  hlhilset  37539