Theorem opeq2d 4165

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

Syntax hints:   -> wi 4   = wceq 1452   <.cop 3965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966

This theorem is referenced by:  fmptsng  6101  fmptsnd  6102  tfrlem11  7124  seqomlem0  7184  seqomlem1  7185  seqomlem4  7188  seqomeq12  7189  fundmen  7661  unxpdomlem1  7794  mulcanenq  9403  elreal2  9574  om2uzrdg  12208  uzrdgsuci  12212  seqeq2  12255  seqeq3  12256  s1val  12790  s1eq  12792  swrdlsw  12862  swrdccatwrd  12878  ccats1swrdeq  12879  ccatopth  12880  wrdeqcats1OLD  12884  swrdccat  12903  swrdccat3blem  12905  swrdccat3b  12906  swrdccatin12d  12911  splval  12912  splcl  12913  cshfn  12946  cshw0  12950  cshwmodn  12951  repswcshw  12968  swrds2  13092  swrd2lsw  13102  eucalgval  14620  setsidvald  15225  ressval  15254  ressress  15265  prdsval  15431  imasval  15489  imasvalOLD  15490  imasaddvallem  15513  cidval  15661  iscatd2  15665  oppcval  15696  ismon  15716  rescval  15810  idfucl  15864  funcres  15879  fucval  15941  fucpropd  15960  setcval  16050  catcval  16069  estrcval  16087  xpcval  16140  1stfcl  16160  2ndfcl  16161  curf12  16190  curf2val  16193  curfcl  16195  hofcl  16222  oduval  16454  ipoval  16478  frmdval  16713  oppgval  17076  symgval  17098  efgmval  17440  efgmnvl  17442  efgi  17447  frgpup3lem  17505  dprd2da  17753  dmdprdpr  17760  dprdpr  17761  pgpfaclem1  17792  mgpval  17804  mgpress  17812  opprval  17930  sraval  18477  rlmval2  18495  psrval  18663  opsrval  18775  opsrval2  18777  zlmval  19164  znval  19183  znval2  19185  thlval  19335  islindf4  19473  matval  19513  mat1dimmul  19578  mat1dimcrng  19579  mat1scmat  19641  mdet0pr  19694  m1detdiag  19699  txkgen  20744  pt1hmeo  20898  xpstopnlem1  20901  tusval  21359  tmsval  21574  tngval  21725  om1val  22139  pi1xfrcnvlem  22165  pi1xfrcnv  22166  dchrval  24241  ttgval  24984  eengv  25088  wwlkextwrd  25535  wwlkextproplem3  25550  clwlkisclwwlk2  25597  clwwlkf1  25603  clwlkfoclwwlk  25652  clwlkf1clwwlklem  25656  clwlkf1clwwlk  25657  clwlksizeeq  25659  eupath2lem3  25786  numclwlk1lem2f1  25901  numclwlk2lem2f1o  25912  br8d  28294  resvval  28664  smatfval  28695  smatrcl  28696  smatlem  28697  fvproj  28733  qqhval  28852  iwrdsplit  29293  bnj66  29743  bnj1234  29894  bnj1296  29902  bnj1450  29931  bnj1463  29936  bnj1501  29948  bnj1523  29952  subfacp1lem5  29979  cvmliftlem10  30089  cvmlift2lem12  30109  msubffval  30233  msubfval  30234  elmsubrn  30238  msubrn  30239  msubco  30241  br8  30467  br6  30468  btwnouttr2  30860  brfs  30917  btwnconn1lem11  30935  csbfinxpg  31850  finixpnum  31994  ldualset  32762  tgrpfset  34382  tgrpset  34383  erngfset  34437  erngset  34438  erngfset-rN  34445  erngset-rN  34446  dvafset  34642  dvaset  34643  dvhfset  34719  dvhset  34720  dvhfvadd  34730  dvhopvadd2  34733  dib1dim2  34807  dicvscacl  34830  cdlemn6  34841  dihopelvalcpre  34887  dih1dimatlem  34968  hdmapfval  35469  hlhilset  35576  mendval  36120  ovolval4lem1  38589  ovolval4lem2  38590  ovnovollem3  38598  pfxpfx  39103  pfxccatin12d  39120  funopsn  39164  uspgr1ewop  39487  usgr2v1e2w  39491  1loopgruspgr  39722  1egrvtxdg1r  39733  1egrvtxdg0  39734  eupth2lem3lem3  40142  eupth2  40151  idfusubc0  40373  idfusubc  40374  rngcvalALTV  40471  ringcvalALTV  40517  zlmodzxzsub  40649  lmod1zr  40794