Theorem opeq2d 4151

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

Syntax hints:   -> wi 4   = wceq 1399   <.cop 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-rab 2751  df-v 3049  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-sn 3958  df-pr 3960  df-op 3964

This theorem is referenced by:  fmptsng  6008  fmptsnd  6009  tfrlem11  6993  seqomlem0  7050  seqomlem1  7051  seqomlem4  7054  seqomeq12  7055  fundmen  7526  unxpdomlem1  7658  mulcanenq  9267  elreal2  9438  om2uzrdg  11989  uzrdgsuci  11993  seqeq2  12033  seqeq3  12034  s1val  12538  s1eq  12540  swrdlsw  12607  swrdccatwrd  12623  ccats1swrdeq  12624  ccatopth  12625  wrdeqcats1OLD  12629  swrdccat  12648  swrdccat3blem  12650  swrdccat3b  12651  swrdccatin12d  12656  splval  12657  splcl  12658  cshfn  12691  cshw0  12695  cshwmodn  12696  repswcshw  12710  swrds2  12813  swrd2lsw  12820  eucalgval  14232  setsidvald  14679  ressval  14707  ressress  14718  prdsval  14881  imasval  14937  imasaddvallem  14955  cidval  15103  iscatd2  15107  oppcval  15138  ismon  15158  rescval  15252  idfucl  15306  funcres  15321  fucval  15383  fucpropd  15402  setcval  15492  catcval  15511  estrcval  15529  xpcval  15582  1stfcl  15602  2ndfcl  15603  curf12  15632  curf2val  15635  curfcl  15637  hofcl  15664  oduval  15896  ipoval  15920  frmdval  16155  oppgval  16518  symgval  16540  efgmval  16866  efgmnvl  16868  efgi  16873  frgpup3lem  16931  dprd2da  17223  dmdprdpr  17230  dprdpr  17231  pgpfaclem1  17264  mgpval  17276  mgpress  17284  opprval  17405  sraval  17954  rlmval2  17972  psrval  18143  opsrval  18271  opsrval2  18273  zlmval  18665  znval  18684  znval2  18686  thlval  18836  islindf4  18977  matval  19017  mat1dimmul  19082  mat1dimcrng  19083  mat1scmat  19145  mdet0pr  19198  m1detdiag  19203  txkgen  20257  pt1hmeo  20411  xpstopnlem1  20414  tusval  20873  tmsval  21088  tngval  21257  om1val  21634  pi1xfrcnvlem  21660  pi1xfrcnv  21661  dchrval  23645  ttgval  24320  eengv  24424  wwlkextwrd  24870  wwlkextproplem3  24885  clwlkisclwwlk2  24932  clwwlkf1  24938  clwlkfoclwwlk  24987  clwlkf1clwwlklem  24991  clwlkf1clwwlk  24992  clwlksizeeq  24994  eupath2lem3  25121  numclwlk1lem2f1  25236  numclwlk2lem2f1o  25247  br8d  27627  resvval  28002  fvproj  28020  qqhval  28139  iwrdsplit  28545  subfacp1lem5  28853  cvmliftlem10  28964  cvmlift2lem12  28984  msubffval  29108  msubfval  29109  elmsubrn  29113  msubrn  29114  msubco  29116  br8  29387  br6  29388  btwnouttr2  29861  brfs  29918  btwnconn1lem11  29936  finixpnum  30239  mendval  31336  pfxpfx  32625  pfxccatin12d  32642  idfusubc0  32906  idfusubc  32907  rngcvalALTV  33004  ringcvalALTV  33050  zlmodzxzsub  33184  lmod1zr  33329  bnj66  34300  bnj1234  34451  bnj1296  34459  bnj1450  34488  bnj1463  34493  bnj1501  34505  bnj1523  34509  ldualset  35298  tgrpfset  36918  tgrpset  36919  erngfset  36973  erngset  36974  erngfset-rN  36981  erngset-rN  36982  dvafset  37178  dvaset  37179  dvhfset  37255  dvhset  37256  dvhfvadd  37266  dvhopvadd2  37269  dib1dim2  37343  dicvscacl  37366  cdlemn6  37377  dihopelvalcpre  37423  dih1dimatlem  37504  hdmapfval  38005  hlhilset  38112