Theorem opeq2d 4063

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

Syntax hints:   -> wi 4   = wceq 1364   <.cop 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881

This theorem is referenced by:  fmptsng  5897  tfrlem11  6843  seqomlem0  6900  seqomlem1  6901  seqomlem4  6904  seqomeq12  6905  fundmen  7379  unxpdomlem1  7513  mulcanenq  9125  elreal2  9295  om2uzrdg  11775  uzrdgsuci  11779  seqeq2  11806  seqeq3  11807  s1val  12286  s1eq  12287  swrdlsw  12342  swrdccatwrd  12358  ccats1swrdeq  12359  ccatopth  12360  wrdeqcats1  12364  swrdccat  12380  swrdccat3blem  12382  swrdccat3b  12383  swrdccatin12d  12388  splval  12389  splcl  12390  cshfn  12423  cshw0  12427  cshwmodn  12428  repswcshw  12442  swrds2  12541  swrd2lsw  12548  eucalgval  13753  ressval  14221  ressress  14231  prdsval  14389  imasval  14445  imasaddvallem  14463  cidval  14611  iscatd2  14615  oppcval  14648  ismon  14668  rescval  14736  idfucl  14787  funcres  14802  fucval  14864  fucpropd  14883  setcval  14941  catcval  14960  xpcval  14983  1stfcl  15003  2ndfcl  15004  curf12  15033  curf2val  15036  curfcl  15038  hofcl  15065  oduval  15296  ipoval  15320  frmdval  15522  oppgval  15855  symgval  15877  efgmval  16202  efgmnvl  16204  efgi  16209  frgpup3lem  16267  dprd2da  16531  dmdprdpr  16538  dprdpr  16539  pgpfaclem1  16572  mgpval  16584  mgpress  16592  opprval  16706  sraval  17235  rlmval2  17253  psrval  17407  opsrval  17532  opsrval2  17534  zlmval  17906  znval  17925  znval2  17929  thlval  18079  islindf4  18226  matval  18270  mdet0pr  18362  txkgen  19184  pt1hmeo  19338  xpstopnlem1  19341  tusval  19800  tmsval  20015  tngval  20184  om1val  20561  pi1xfrcnvlem  20587  pi1xfrcnv  20588  dchrval  22532  ttgval  23056  eengv  23160  eupath2lem3  23535  br8d  25877  resvval  26231  qqhval  26339  iwrdsplit  26700  subfacp1lem5  27002  cvmliftlem10  27113  cvmlift2lem12  27133  br8  27495  br6  27496  btwnouttr2  27982  brfs  28039  btwnconn1lem11  28057  finixpnum  28339  mendval  29465  wwlkextwrd  30285  clwlkisclwwlk2  30377  clwwlkf1  30383  clwlkfoclwwlk  30443  clwlkf1clwwlklem  30447  clwlkf1clwwlk  30448  clwlksizeeq  30450  wwlkextproplem3  30487  numclwlk1lem2f1  30612  numclwlk2lem2f1o  30623  fmptsnd  30646  zlmodzxzsub  30674  mat1dimmul  30755  mat1dimcrng  30756  m1detdiag  30775  lmod1zr  30876  bnj66  31687  bnj1234  31838  bnj1296  31846  bnj1450  31875  bnj1463  31880  bnj1501  31892  bnj1523  31896  ldualset  32492  tgrpfset  34110  tgrpset  34111  erngfset  34165  erngset  34166  erngfset-rN  34173  erngset-rN  34174  dvafset  34370  dvaset  34371  dvhfset  34447  dvhset  34448  dvhfvadd  34458  dvhopvadd2  34461  dib1dim2  34535  dicvscacl  34558  cdlemn6  34569  dihopelvalcpre  34615  dih1dimatlem  34696  hdmapfval  35197  hlhilset  35304