MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpteq1d Structured version   Visualization version   GIF version

Theorem mpteq1d 5201
Description: An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)
Hypothesis
Ref Expression
mpteq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
mpteq1d (𝜑 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝐶(𝑥)

Proof of Theorem mpteq1d
StepHypRef Expression
1 mpteq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 mpteq1 5199 . 2 (𝐴 = 𝐵 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  cmpt 5189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-opab 5169  df-mpt 5190
This theorem is referenced by:  csbmpt2  5516  fmptapd  7118  offval  7627  mposn  8036  offsplitfpar  8052  mpocurryd  8201  cantnff  9611  dfac12lem1  10080  ackbij2lem2  10177  swrd00  14533  swrdlend  14542  swrd0  14547  repswswrd  14673  repswrevw  14676  revco  14724  ccatco  14725  ofccat  14855  vdwapfval  16844  imasdsval  17398  mrcfval  17489  catidd  17561  curfpropd  18123  pwspjmhm  18641  grpinvfval  18790  grpinvfvalALT  18791  psgnfval  19283  psgnfvalfi  19296  odfval  19315  odfvalALT  19316  frgpup3lem  19560  gsum2d2  19752  gsumxp  19754  telgsumfzs  19767  dprd2d2  19824  srgbinom  19963  gsummgp0  20033  pwsco1rhm  20173  pwsco2rhm  20174  staffval  20309  phlpropd  21062  pjfval  21115  asclfval  21285  asclpropd  21303  mpfrcl  21498  evlsval  21499  evls1rhmlem  21690  evl1fval  21697  mvmulfval  21894  submafval  21931  mdetfval  21938  nfimdetndef  21941  mdetfval1  21942  mdet0pr  21944  m1detdiag  21949  madufval  21989  minmar1fval  21998  gsummatr01  22011  pmatcollpw3fi1lem2  22139  pmatcollpw3fi1  22140  cpmadugsumlemF  22228  ispnrm  22693  ptval2  22955  ptpjcn  22965  xkoptsub  23008  kqval  23080  pt1hmeo  23160  fmval  23297  tmdgsum  23449  subgtgp  23459  prdstmdd  23478  prdsxmslem2  23888  nmfval  23947  lebnumlem1  24327  limcmpt2  25251  dvcmulf  25312  mdegfval  25430  ulmshft  25752  wwlksnextbij  28850  off2  31560  mptprop  31615  gsummpt2co  31893  gsumhashmul  31901  freshmansdream  32070  elrspunidl  32206  esumnul  32650  ofcfval4  32707  measdivcst  32826  omsfval  32897  signstfval  33179  signstf0  33183  signstfvn  33184  mrsubffval  34104  mrsubfval  34105  msubfval  34121  elmsubrn  34125  mvhfval  34130  msrfval  34134  fwddifval  34750  tailfval  34847  curf  36059  poimirlem24  36105  ftc1anc  36162  sdclem2  36204  erngfset  39265  erngfset-rN  39273  dvhfset  39546  dvhset  39547  aks4d1p1p6  40533  sticksstones11  40567  fsuppssindlem2  40770  fsuppssind  40771  mzpclval  41051  mzpcompact2  41078  fsovrfovd  42288  mptima2  43480  supcnvlimsupmpt  43989  cncfshiftioo  44140  cncfiooicc  44142  dvsinax  44161  iblspltprt  44221  itgspltprt  44227  itgiccshift  44228  dirkercncflem2  44352  fourierdlem90  44444  fourierdlem92  44446  sge0val  44614  sge0prle  44649  sge0ss  44660  sge0iunmptlemfi  44661  sge0p1  44662  sge0iunmptlemre  44663  sge0iunmpt  44666  sge0xp  44677  ismeannd  44715  caratheodorylem1  44774  isomenndlem  44778  hoidmv1lelem2  44840  hoidmvlelem2  44844  hspmbllem2  44875  smflimsuplem1  45068  smflimsuplem4  45071  smflimsuplem7  45074  smflimsup  45076  funcrngcsetc  46303  funcrngcsetcALT  46304  funcringcsetc  46340  mgpsumunsn  46444  lmod1zr  46581
  Copyright terms: Public domain W3C validator