MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opeq2d Structured version   Unicode version

Theorem opeq2d 3993
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
StepHypRef Expression
1 opeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 opeq2 3987 . 2  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
31, 2syl 16 1  |-  ( ph  -> 
<. C ,  A >.  = 
<. C ,  B >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   <.cop 3819
This theorem is referenced by:  tfrlem11  6652  seqomlem0  6709  seqomlem1  6710  seqomlem4  6713  seqomeq12  6714  fundmen  7183  unxpdomlem1  7316  mulcanenq  8842  elreal2  9012  om2uzrdg  11301  uzrdgsuci  11305  seqeq2  11332  seqeq3  11333  s1val  11757  s1eq  11758  ccatopth  11781  splval  11785  splcl  11786  wrdeqcats1  11793  swrds2  11885  eucalgval  13078  ressval  13521  ressress  13531  prdsval  13683  imasval  13742  imasaddvallem  13759  cidval  13907  iscatd2  13911  oppcval  13944  ismon  13964  rescval  14032  idfucl  14083  funcres  14098  fucval  14160  fucpropd  14179  setcval  14237  catcval  14256  xpcval  14279  1stfcl  14299  2ndfcl  14300  curf12  14329  curf2val  14332  curfcl  14334  hofcl  14361  oduval  14562  ipoval  14585  frmdval  14801  symgval  15099  oppgval  15148  efgmval  15349  efgmnvl  15351  efgi  15356  frgpup3lem  15414  dprd2da  15605  dmdprdpr  15612  dprdpr  15613  pgpfaclem1  15644  mgpval  15656  mgpress  15664  opprval  15734  sraval  16253  psrval  16434  opsrval  16540  opsrval2  16542  zlmval  16802  znval  16821  znval2  16823  thlval  16927  txkgen  17689  pt1hmeo  17843  xpstopnlem1  17846  tusval  18301  tmsval  18516  tngval  18685  om1val  19060  pi1xfrcnvlem  19086  pi1xfrcnv  19087  dchrval  21023  eupath2lem3  21706  qqhval  24363  subfacp1lem5  24875  cvmliftlem10  24986  cvmlift2lem12  25006  br8  25384  br6  25385  btwnouttr2  25961  brfs  26018  btwnconn1lem11  26036  islindf4  27299  matval  27456  mendval  27482  swrd0swrdid  28234  swrdccat  28250  swrdccat3blem  28252  swrdccat3b  28253  swrdccatin12d  28256  2cshw1lem1  28282  2cshw1lem2  28283  2cshw1lem3  28284  2cshw1  28285  2cshw2lem2  28287  2cshw2  28289  bnj66  29305  bnj1234  29456  bnj1296  29464  bnj1450  29493  bnj1463  29498  bnj1501  29510  bnj1523  29514  ldualset  29997  tgrpfset  31615  tgrpset  31616  erngfset  31670  erngset  31671  erngfset-rN  31678  erngset-rN  31679  dvafset  31875  dvaset  31876  dvhfset  31952  dvhset  31953  dvhfvadd  31963  dvhopvadd2  31966  dib1dim2  32040  dicvscacl  32063  cdlemn6  32074  dihopelvalcpre  32120  dih1dimatlem  32201  hdmapfval  32702  hlhilset  32809
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825
  Copyright terms: Public domain W3C validator