Theorem opeq2d 4078

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

Syntax hints:   -> wi 4   = wceq 1369   <.cop 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896

This theorem is referenced by:  fmptsng  5912  tfrlem11  6859  seqomlem0  6916  seqomlem1  6917  seqomlem4  6920  seqomeq12  6921  fundmen  7395  unxpdomlem1  7529  mulcanenq  9141  elreal2  9311  om2uzrdg  11791  uzrdgsuci  11795  seqeq2  11822  seqeq3  11823  s1val  12302  s1eq  12303  swrdlsw  12358  swrdccatwrd  12374  ccats1swrdeq  12375  ccatopth  12376  wrdeqcats1  12380  swrdccat  12396  swrdccat3blem  12398  swrdccat3b  12399  swrdccatin12d  12404  splval  12405  splcl  12406  cshfn  12439  cshw0  12443  cshwmodn  12444  repswcshw  12458  swrds2  12557  swrd2lsw  12564  eucalgval  13769  ressval  14237  ressress  14247  prdsval  14405  imasval  14461  imasaddvallem  14479  cidval  14627  iscatd2  14631  oppcval  14664  ismon  14684  rescval  14752  idfucl  14803  funcres  14818  fucval  14880  fucpropd  14899  setcval  14957  catcval  14976  xpcval  14999  1stfcl  15019  2ndfcl  15020  curf12  15049  curf2val  15052  curfcl  15054  hofcl  15081  oduval  15312  ipoval  15336  frmdval  15541  oppgval  15874  symgval  15896  efgmval  16221  efgmnvl  16223  efgi  16228  frgpup3lem  16286  dprd2da  16553  dmdprdpr  16560  dprdpr  16561  pgpfaclem1  16594  mgpval  16606  mgpress  16614  opprval  16728  sraval  17269  rlmval2  17287  psrval  17441  opsrval  17568  opsrval2  17570  zlmval  17959  znval  17978  znval2  17982  thlval  18132  islindf4  18279  matval  18323  mdet0pr  18415  txkgen  19237  pt1hmeo  19391  xpstopnlem1  19394  tusval  19853  tmsval  20068  tngval  20237  om1val  20614  pi1xfrcnvlem  20640  pi1xfrcnv  20641  dchrval  22585  ttgval  23133  eengv  23237  eupath2lem3  23612  br8d  25954  resvval  26307  qqhval  26415  iwrdsplit  26782  subfacp1lem5  27084  cvmliftlem10  27195  cvmlift2lem12  27215  br8  27578  br6  27579  btwnouttr2  28065  brfs  28122  btwnconn1lem11  28140  finixpnum  28426  mendval  29552  wwlkextwrd  30372  clwlkisclwwlk2  30464  clwwlkf1  30470  clwlkfoclwwlk  30530  clwlkf1clwwlklem  30534  clwlkf1clwwlk  30535  clwlksizeeq  30537  wwlkextproplem3  30574  numclwlk1lem2f1  30699  numclwlk2lem2f1o  30710  fmptsnd  30734  zlmodzxzsub  30769  mat1dimmul  30884  mat1dimcrng  30885  m1detdiag  30946  lmod1zr  31047  bnj66  31865  bnj1234  32016  bnj1296  32024  bnj1450  32053  bnj1463  32058  bnj1501  32070  bnj1523  32074  ldualset  32782  tgrpfset  34400  tgrpset  34401  erngfset  34455  erngset  34456  erngfset-rN  34463  erngset-rN  34464  dvafset  34660  dvaset  34661  dvhfset  34737  dvhset  34738  dvhfvadd  34748  dvhopvadd2  34751  dib1dim2  34825  dicvscacl  34848  cdlemn6  34859  dihopelvalcpre  34905  dih1dimatlem  34986  hdmapfval  35487  hlhilset  35594