Theorem opeq2d 4220

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

Syntax hints:   -> wi 4   = wceq 1379   <.cop 4033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034

This theorem is referenced by:  fmptsng  6080  fmptsnd  6081  tfrlem11  7054  seqomlem0  7111  seqomlem1  7112  seqomlem4  7115  seqomeq12  7116  fundmen  7586  unxpdomlem1  7721  mulcanenq  9334  elreal2  9505  om2uzrdg  12030  uzrdgsuci  12034  seqeq2  12074  seqeq3  12075  s1val  12568  s1eq  12569  swrdlsw  12634  swrdccatwrd  12650  ccats1swrdeq  12651  ccatopth  12652  wrdeqcats1  12656  swrdccat  12675  swrdccat3blem  12677  swrdccat3b  12678  swrdccatin12d  12683  splval  12684  splcl  12685  cshfn  12718  cshw0  12722  cshwmodn  12723  repswcshw  12737  swrds2  12840  swrd2lsw  12847  eucalgval  14063  ressval  14535  ressress  14545  prdsval  14703  imasval  14759  imasaddvallem  14777  cidval  14925  iscatd2  14929  oppcval  14962  ismon  14982  rescval  15050  idfucl  15101  funcres  15116  fucval  15178  fucpropd  15197  setcval  15255  catcval  15274  xpcval  15297  1stfcl  15317  2ndfcl  15318  curf12  15347  curf2val  15350  curfcl  15352  hofcl  15379  oduval  15610  ipoval  15634  frmdval  15839  oppgval  16174  symgval  16196  efgmval  16523  efgmnvl  16525  efgi  16530  frgpup3lem  16588  dprd2da  16878  dmdprdpr  16885  dprdpr  16886  pgpfaclem1  16919  mgpval  16931  mgpress  16939  opprval  17054  sraval  17602  rlmval2  17620  psrval  17779  opsrval  17907  opsrval2  17909  zlmval  18317  znval  18336  znval2  18340  thlval  18490  islindf4  18637  matval  18677  mat1dimmul  18742  mat1dimcrng  18743  mat1scmat  18805  mdet0pr  18858  m1detdiag  18863  txkgen  19885  pt1hmeo  20039  xpstopnlem1  20042  tusval  20501  tmsval  20716  tngval  20885  om1val  21262  pi1xfrcnvlem  21288  pi1xfrcnv  21289  dchrval  23234  ttgval  23851  eengv  23955  wwlkextwrd  24401  wwlkextproplem3  24416  clwlkisclwwlk2  24463  clwwlkf1  24469  clwlkfoclwwlk  24518  clwlkf1clwwlklem  24522  clwlkf1clwwlk  24523  clwlksizeeq  24525  eupath2lem3  24652  numclwlk1lem2f1  24768  numclwlk2lem2f1o  24779  br8d  27133  resvval  27477  fvproj  27495  qqhval  27588  iwrdsplit  27963  subfacp1lem5  28265  cvmliftlem10  28376  cvmlift2lem12  28396  br8  28759  br6  28760  btwnouttr2  29246  brfs  29303  btwnconn1lem11  29321  finixpnum  29612  mendval  30737  zlmodzxzsub  32013  lmod1zr  32175  bnj66  32997  bnj1234  33148  bnj1296  33156  bnj1450  33185  bnj1463  33190  bnj1501  33202  bnj1523  33206  ldualset  33922  tgrpfset  35540  tgrpset  35541  erngfset  35595  erngset  35596  erngfset-rN  35603  erngset-rN  35604  dvafset  35800  dvaset  35801  dvhfset  35877  dvhset  35878  dvhfvadd  35888  dvhopvadd2  35891  dib1dim2  35965  dicvscacl  35988  cdlemn6  35999  dihopelvalcpre  36045  dih1dimatlem  36126  hdmapfval  36627  hlhilset  36734