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

Theorem mpteq1d 4925
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 4924 . 2 (𝐴 = 𝐵 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  cmpt 4916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-ext 2781
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-ral 3097  df-opab 4900  df-mpt 4917
This theorem is referenced by:  csbmpt2  5200  fmptapd  6656  offval  7128  mpt2sn  7496  mpt2curryd  7624  cantnff  8812  dfac12lem1  9244  ackbij2lem2  9341  swrd00  13635  swrd0val  13638  swrdlend  13649  swrd0  13652  repswswrd  13749  repswrevw  13751  revco  13798  ccatco  13799  ofccat  13927  vdwapfval  15886  imasdsval  16374  mrcfval  16467  catidd  16539  curfpropd  17072  pwspjmhm  17567  grpinvfval  17659  psgnfval  18115  psgnfvalfi  18128  odfval  18147  frgpup3lem  18385  gsum2d2  18568  gsumxp  18570  telgsumfzs  18582  dprd2d2  18639  srgbinom  18741  gsummgp0  18804  pwsco1rhm  18936  pwsco2rhm  18937  staffval  19045  asclfval  19537  asclpropd  19549  mpfrcl  19720  evlsval  19721  evls1rhmlem  19888  evl1fval  19894  phlpropd  20204  pjfval  20254  mvmulfval  20553  submafval  20590  mdetfval  20597  nfimdetndef  20600  mdetfval1  20601  mdet0pr  20603  m1detdiag  20608  madufval  20648  minmar1fval  20657  gsummatr01  20671  pmatcollpw3fi1lem2  20799  pmatcollpw3fi1  20800  cpmadugsumlemF  20888  ispnrm  21351  ptval2  21612  ptpjcn  21622  xkoptsub  21665  kqval  21737  pt1hmeo  21817  fmval  21954  tmdgsum  22106  subgtgp  22116  prdstmdd  22134  prdsxmslem2  22541  nmfval  22600  lebnumlem1  22967  limcmpt2  23856  dvcmulf  23916  mdegfval  24030  ulmshft  24352  wwlksnextbij  27033  off2  29764  gsummpt2co  30099  esumnul  30429  ofcfval4  30486  measdivcst  30607  omsfval  30675  signstfval  30960  signstf0  30964  signstfvn  30965  mrsubffval  31721  mrsubfval  31722  msubfval  31738  elmsubrn  31742  mvhfval  31747  msrfval  31751  fwddifval  32584  tailfval  32682  curf  33694  poimirlem24  33740  ftc1anc  33799  sdclem2  33843  erngfset  36574  erngfset-rN  36582  dvhfset  36855  dvhset  36856  mzpclval  37784  mzpcompact2  37811  fsovrfovd  38797  mptima2  39935  supcnvlimsupmpt  40447  cncfshiftioo  40579  cncfiooicc  40581  dvsinax  40601  iblspltprt  40662  itgspltprt  40668  itgiccshift  40669  dirkercncflem2  40794  fourierdlem90  40886  fourierdlem92  40888  sge0val  41056  sge0prle  41091  sge0ss  41102  sge0iunmptlemfi  41103  sge0p1  41104  sge0iunmptlemre  41105  sge0iunmpt  41108  sge0xp  41119  ismeannd  41157  caratheodorylem1  41216  isomenndlem  41220  hoidmv1lelem2  41282  hoidmvlelem2  41286  hspmbllem2  41317  smflimsuplem1  41502  smflimsuplem4  41505  smflimsuplem7  41508  smflimsup  41510  funcrngcsetc  42560  funcrngcsetcALT  42561  funcringcsetc  42597  mgpsumunsn  42702  lmod1zr  42844
  Copyright terms: Public domain W3C validator