Theorem opeq2d 3951

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

Syntax hints:   -> wi 4   = wceq 1649   <.cop 3777

This theorem is referenced by:  tfrlem11  6608  seqomlem0  6665  seqomlem1  6666  seqomlem4  6669  seqomeq12  6670  fundmen  7139  unxpdomlem1  7272  mulcanenq  8793  elreal2  8963  om2uzrdg  11251  uzrdgsuci  11255  seqeq2  11282  seqeq3  11283  s1val  11707  s1eq  11708  ccatopth  11731  splval  11735  splcl  11736  wrdeqcats1  11743  swrds2  11835  eucalgval  13028  ressval  13471  ressress  13481  prdsval  13633  imasval  13692  imasaddvallem  13709  cidval  13857  iscatd2  13861  oppcval  13894  ismon  13914  rescval  13982  idfucl  14033  funcres  14048  fucval  14110  fucpropd  14129  setcval  14187  catcval  14206  xpcval  14229  1stfcl  14249  2ndfcl  14250  curf12  14279  curf2val  14282  curfcl  14284  hofcl  14311  oduval  14512  ipoval  14535  frmdval  14751  symgval  15049  oppgval  15098  efgmval  15299  efgmnvl  15301  efgi  15306  frgpup3lem  15364  dprd2da  15555  dmdprdpr  15562  dprdpr  15563  pgpfaclem1  15594  mgpval  15606  mgpress  15614  opprval  15684  sraval  16203  psrval  16384  opsrval  16490  opsrval2  16492  zlmval  16752  znval  16771  znval2  16773  thlval  16877  txkgen  17637  pt1hmeo  17791  xpstopnlem1  17794  tusval  18249  tmsval  18464  tngval  18633  om1val  19008  pi1xfrcnvlem  19034  pi1xfrcnv  19035  dchrval  20971  eupath2lem3  21654  qqhval  24311  subfacp1lem5  24823  cvmliftlem10  24934  cvmlift2lem12  24954  br8  25327  br6  25328  btwnouttr2  25860  brfs  25917  btwnconn1lem11  25935  islindf4  27176  matval  27333  mendval  27359  swrd0swrdid  28012  swrdccatin12b  28027  swrdccatin12c  28028  swrdccat3b  28031  bnj66  28937  bnj1234  29088  bnj1296  29096  bnj1450  29125  bnj1463  29130  bnj1501  29142  bnj1523  29146  ldualset  29608  tgrpfset  31226  tgrpset  31227  erngfset  31281  erngset  31282  erngfset-rN  31289  erngset-rN  31290  dvafset  31486  dvaset  31487  dvhfset  31563  dvhset  31564  dvhfvadd  31574  dvhopvadd2  31577  dib1dim2  31651  dicvscacl  31674  cdlemn6  31685  dihopelvalcpre  31731  dih1dimatlem  31812  hdmapfval  32313  hlhilset  32420

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783