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

Theorem opeq2d 3978
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 3972 . 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 1652   <.cop 3804
This theorem is referenced by:  tfrlem11  6635  seqomlem0  6692  seqomlem1  6693  seqomlem4  6696  seqomeq12  6697  fundmen  7166  unxpdomlem1  7299  mulcanenq  8821  elreal2  8991  om2uzrdg  11279  uzrdgsuci  11283  seqeq2  11310  seqeq3  11311  s1val  11735  s1eq  11736  ccatopth  11759  splval  11763  splcl  11764  wrdeqcats1  11771  swrds2  11863  eucalgval  13056  ressval  13499  ressress  13509  prdsval  13661  imasval  13720  imasaddvallem  13737  cidval  13885  iscatd2  13889  oppcval  13922  ismon  13942  rescval  14010  idfucl  14061  funcres  14076  fucval  14138  fucpropd  14157  setcval  14215  catcval  14234  xpcval  14257  1stfcl  14277  2ndfcl  14278  curf12  14307  curf2val  14310  curfcl  14312  hofcl  14339  oduval  14540  ipoval  14563  frmdval  14779  symgval  15077  oppgval  15126  efgmval  15327  efgmnvl  15329  efgi  15334  frgpup3lem  15392  dprd2da  15583  dmdprdpr  15590  dprdpr  15591  pgpfaclem1  15622  mgpval  15634  mgpress  15642  opprval  15712  sraval  16231  psrval  16412  opsrval  16518  opsrval2  16520  zlmval  16780  znval  16799  znval2  16801  thlval  16905  txkgen  17667  pt1hmeo  17821  xpstopnlem1  17824  tusval  18279  tmsval  18494  tngval  18663  om1val  19038  pi1xfrcnvlem  19064  pi1xfrcnv  19065  dchrval  21001  eupath2lem3  21684  qqhval  24341  subfacp1lem5  24853  cvmliftlem10  24964  cvmlift2lem12  24984  br8  25363  br6  25364  btwnouttr2  25899  brfs  25956  btwnconn1lem11  25974  islindf4  27218  matval  27375  mendval  27401  swrd0swrdid  28054  swrdccatin12b  28069  swrdccatin12c  28070  swrdccat3b  28073  bnj66  28983  bnj1234  29134  bnj1296  29142  bnj1450  29171  bnj1463  29176  bnj1501  29188  bnj1523  29192  ldualset  29654  tgrpfset  31272  tgrpset  31273  erngfset  31327  erngset  31328  erngfset-rN  31335  erngset-rN  31336  dvafset  31532  dvaset  31533  dvhfset  31609  dvhset  31610  dvhfvadd  31620  dvhopvadd2  31623  dib1dim2  31697  dicvscacl  31720  cdlemn6  31731  dihopelvalcpre  31777  dih1dimatlem  31858  hdmapfval  32359  hlhilset  32466
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-rab 2701  df-v 2945  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-sn 3807  df-pr 3808  df-op 3810
  Copyright terms: Public domain W3C validator