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

Theorem opeq2d 3819
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 3813 . 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 1632   <.cop 3656
This theorem is referenced by:  tfrlem11  6420  seqomlem0  6477  seqomlem1  6478  seqomlem4  6481  seqomeq12  6482  fundmen  6950  unxpdomlem1  7083  mulcanenq  8600  elreal2  8770  om2uzrdg  11035  uzrdgsuci  11039  seqeq2  11066  seqeq3  11067  s1val  11454  s1eq  11455  ccatopth  11478  splval  11482  splcl  11483  wrdeqcats1  11490  swrds2  11576  eucalgval  12768  ressval  13211  ressress  13221  prdsval  13371  imasval  13430  imasaddvallem  13447  cidval  13595  iscatd2  13599  oppcval  13632  ismon  13652  rescval  13720  idfucl  13771  funcres  13786  fucval  13848  fucpropd  13867  setcval  13925  catcval  13944  xpcval  13967  1stfcl  13987  2ndfcl  13988  curf12  14017  curf2val  14020  curfcl  14022  hofcl  14049  oduval  14250  ipoval  14273  frmdval  14489  symgval  14787  oppgval  14836  efgmval  15037  efgmnvl  15039  efgi  15044  frgpup3lem  15102  dprd2da  15293  dmdprdpr  15300  dprdpr  15301  pgpfaclem1  15332  mgpval  15344  mgpress  15352  opprval  15422  sraval  15945  psrval  16126  opsrval  16232  opsrval2  16234  zlmval  16486  znval  16505  znval2  16507  thlval  16611  txkgen  17362  pt1hmeo  17513  xpstopnlem1  17516  tmsval  18043  tngval  18171  om1val  18544  pi1xfrcnvlem  18570  pi1xfrcnv  18571  dchrval  20489  subfacp1lem5  23730  cvmliftlem10  23840  cvmlift2lem12  23860  eupath2lem3  23918  br8  24184  br6  24185  btwnouttr2  24717  brfs  24774  btwnconn1lem11  24792  isder  25810  isded  25839  dedi  25840  iscatOLD  25857  cati  25858  cmp2morpcatt  26065  cmpmorass  26069  morexcmp2  26071  cmpidmor2  26072  islindf4  27411  matval  27568  mendval  27594  bnj66  29208  bnj1234  29359  bnj1296  29367  bnj1450  29396  bnj1463  29401  bnj1501  29413  bnj1523  29417  ldualset  29937  tgrpfset  31555  tgrpset  31556  erngfset  31610  erngset  31611  erngfset-rN  31618  erngset-rN  31619  dvafset  31815  dvaset  31816  dvhfset  31892  dvhset  31893  dvhfvadd  31903  dvhopvadd2  31906  dib1dim2  31980  dicvscacl  32003  cdlemn6  32014  dihopelvalcpre  32060  dih1dimatlem  32141  hdmapfval  32642  hlhilset  32749
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662
  Copyright terms: Public domain W3C validator