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

Theorem mpteq1d 5152
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 5151 . 2 (𝐴 = 𝐵 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  cmpt 5143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-ral 3148  df-opab 5126  df-mpt 5144
This theorem is referenced by:  csbmpt2  5442  fmptapd  6929  offval  7406  mposn  7789  offsplitfpar  7806  mpocurryd  7926  cantnff  9126  dfac12lem1  9558  ackbij2lem2  9651  swrd00  13996  swrdlend  14005  swrd0  14010  repswswrd  14136  repswrevw  14139  revco  14186  ccatco  14187  ofccat  14319  vdwapfval  16297  imasdsval  16778  mrcfval  16869  catidd  16941  curfpropd  17473  pwspjmhm  17977  grpinvfval  18072  grpinvfvalALT  18073  psgnfval  18548  psgnfvalfi  18561  odfval  18580  odfvalALT  18581  frgpup3lem  18823  gsum2d2  19014  gsumxp  19016  telgsumfzs  19029  dprd2d2  19086  srgbinom  19215  gsummgp0  19278  pwsco1rhm  19410  pwsco2rhm  19411  staffval  19538  asclfval  20027  asclpropd  20045  mpfrcl  20217  evlsval  20218  evls1rhmlem  20403  evl1fval  20410  phlpropd  20718  pjfval  20769  mvmulfval  21070  submafval  21107  mdetfval  21114  nfimdetndef  21117  mdetfval1  21118  mdet0pr  21120  m1detdiag  21125  madufval  21165  minmar1fval  21174  gsummatr01  21187  pmatcollpw3fi1lem2  21314  pmatcollpw3fi1  21315  cpmadugsumlemF  21403  ispnrm  21866  ptval2  22128  ptpjcn  22138  xkoptsub  22181  kqval  22253  pt1hmeo  22333  fmval  22470  tmdgsum  22622  subgtgp  22632  prdstmdd  22650  prdsxmslem2  23057  nmfval  23116  lebnumlem1  23483  limcmpt2  24400  dvcmulf  24460  mdegfval  24574  ulmshft  24896  wwlksnextbij  27597  off2  30306  mptprop  30350  gsummpt2co  30603  freshmansdream  30776  esumnul  31196  ofcfval4  31253  measdivcst  31372  omsfval  31441  signstfval  31723  signstf0  31727  signstfvn  31728  mrsubffval  32641  mrsubfval  32642  msubfval  32658  elmsubrn  32662  mvhfval  32667  msrfval  32671  fwddifval  33510  tailfval  33607  curf  34740  poimirlem24  34786  ftc1anc  34845  sdclem2  34888  erngfset  37805  erngfset-rN  37813  dvhfset  38086  dvhset  38087  mzpclval  39190  mzpcompact2  39217  fsovrfovd  40223  mptima2  41385  supcnvlimsupmpt  41890  cncfshiftioo  42043  cncfiooicc  42045  dvsinax  42065  iblspltprt  42126  itgspltprt  42132  itgiccshift  42133  dirkercncflem2  42258  fourierdlem90  42350  fourierdlem92  42352  sge0val  42517  sge0prle  42552  sge0ss  42563  sge0iunmptlemfi  42564  sge0p1  42565  sge0iunmptlemre  42566  sge0iunmpt  42569  sge0xp  42580  ismeannd  42618  caratheodorylem1  42677  isomenndlem  42681  hoidmv1lelem2  42743  hoidmvlelem2  42747  hspmbllem2  42778  smflimsuplem1  42963  smflimsuplem4  42966  smflimsuplem7  42969  smflimsup  42971  funcrngcsetc  44104  funcrngcsetcALT  44105  funcringcsetc  44141  mgpsumunsn  44244  lmod1zr  44383
  Copyright terms: Public domain W3C validator