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

Theorem opeq2d 3803
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 3797 . 2  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
31, 2syl 15 1  |-  ( ph  -> 
<. C ,  A >.  = 
<. C ,  B >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   <.cop 3643
This theorem is referenced by:  tfrlem11  6404  seqomlem0  6461  seqomlem1  6462  seqomlem4  6465  seqomeq12  6466  fundmen  6934  unxpdomlem1  7067  mulcanenq  8584  elreal2  8754  om2uzrdg  11019  uzrdgsuci  11023  seqeq2  11050  seqeq3  11051  s1val  11438  s1eq  11439  ccatopth  11462  splval  11466  splcl  11467  wrdeqcats1  11474  swrds2  11560  eucalgval  12752  ressval  13195  ressress  13205  prdsval  13355  imasval  13414  imasaddvallem  13431  cidval  13579  iscatd2  13583  oppcval  13616  ismon  13636  rescval  13704  idfucl  13755  funcres  13770  fucval  13832  fucpropd  13851  setcval  13909  catcval  13928  xpcval  13951  1stfcl  13971  2ndfcl  13972  curf12  14001  curf2val  14004  curfcl  14006  hofcl  14033  oduval  14234  ipoval  14257  frmdval  14473  symgval  14771  oppgval  14820  efgmval  15021  efgmnvl  15023  efgi  15028  frgpup3lem  15086  dprd2da  15277  dmdprdpr  15284  dprdpr  15285  pgpfaclem1  15316  mgpval  15328  mgpress  15336  opprval  15406  sraval  15929  psrval  16110  opsrval  16216  opsrval2  16218  zlmval  16470  znval  16489  znval2  16491  thlval  16595  txkgen  17346  pt1hmeo  17497  xpstopnlem1  17500  tmsval  18027  tngval  18155  om1val  18528  pi1xfrcnvlem  18554  pi1xfrcnv  18555  dchrval  20473  subfacp1lem5  23715  cvmliftlem10  23825  cvmlift2lem12  23845  eupath2lem3  23903  br8  24113  br6  24114  btwnouttr2  24645  brfs  24702  btwnconn1lem11  24720  isder  25707  isded  25736  dedi  25737  iscatOLD  25754  cati  25755  cmp2morpcatt  25962  cmpmorass  25966  morexcmp2  25968  cmpidmor2  25969  islindf4  27308  matval  27465  mendval  27491  bnj66  28892  bnj1234  29043  bnj1296  29051  bnj1450  29080  bnj1463  29085  bnj1501  29097  bnj1523  29101  ldualset  29315  tgrpfset  30933  tgrpset  30934  erngfset  30988  erngset  30989  erngfset-rN  30996  erngset-rN  30997  dvafset  31193  dvaset  31194  dvhfset  31270  dvhset  31271  dvhfvadd  31281  dvhopvadd2  31284  dib1dim2  31358  dicvscacl  31381  cdlemn6  31392  dihopelvalcpre  31438  dih1dimatlem  31519  hdmapfval  32020  hlhilset  32127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649
  Copyright terms: Public domain W3C validator