Theorem mpteq1d 5206

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

Step	Hyp	Ref	Expression
1		mpteq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		mpteq1 5205	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ↦ cmpt 5197

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-opab 5179  df-mpt 5198

This theorem is used by:  csbmpt2  5548  mptimass  6080  fmptapd  7176  offval  7696  mposn  8107  offsplitfpar  8123  mpocurryd  8274  cantnff  9653  dfac12lem1  10146  ackbij2lem2  10241  swrd00  14704  swrdlend  14715  swrd0  14720  repswswrd  14847  repswrevw  14850  revco  14897  ccatco  14898  ofccat  15032  vdwapfval  17056  imasdsval  17594  mrcfval  17689  catidd  17761  curfpropd  18314  pwspjmhm  18920  grpinvfval  19076  grpinvfvalALT  19077  psgnfval  19601  psgnfvalfi  19614  odfval  19633  odfvalALT  19634  frgpup3lem  19878  gsum2d2  20075  gsumxp  20077  telgsumfzs  20090  dprd2d2  20147  srgbinom  20344  gsummgp0  20432  pwsco1rhm  20626  pwsco2rhm  20627  funcrngcsetc  20776  funcrngcsetcALT  20777  funcringcsetc  20810  staffval  20981  freshmansdream  21761  phlpropd  21842  pjfval  21893  asclfval  22065  asclpropd  22084  mpfrcl  22273  evlsval  22274  psdffval  22357  evls1rhmlem  22518  evl1fval  22525  mvmulfval  22736  submafval  22773  mdetfval  22780  nfimdetndef  22783  mdetfval1  22784  mdet0pr  22786  m1detdiag  22791  madufval  22831  minmar1fval  22840  gsummatr01  22853  pmatcollpw3fi1lem2  22981  pmatcollpw3fi1  22982  cpmadugsumlemF  23070  ispnrm  23533  ptval2  23795  ptpjcn  23805  xkoptsub  23848  kqval  23920  pt1hmeo  24000  fmval  24137  tmdgsum  24289  subgtgp  24299  prdstmdd  24318  prdsxmslem2  24723  nmfval  24782  lebnumlem1  25157  limcmpt2  26080  dvcmulf  26141  mdegfval  26256  ulmshft  26590  wwlksnextbij  30288  off2  33023  of0r  33061  mptiffisupp  33075  mptprop  33080  fmptunsnop  33082  gsummpt2co  33399  gsumhashmul  33418  gsummulsubdishift1  33419  gsumwrd2dccat  33429  elrgspnlem4  33596  elrspunidl  33767  evl1deg2  33898  ply1coedeg  33910  gsummoncoe1fz  33919  0mplrim  33935  splyval  33980  vietalem  34000  vieta  34001  algextdeglem4  34141  esumnul  34469  ofcfval4  34526  measdivcst  34646  omsfval  34716  signstfval  34983  signstf0  34987  signstfvn  34988  mrsubffval  36020  mrsubfval  36021  msubfval  36037  elmsubrn  36041  mvhfval  36046  msrfval  36050  fwddifval  36675  tailfval  36924  curf  38290  poimirlem24  38336  ftc1anc  38393  sdclem2  38434  erngfset  41614  erngfset-rN  41622  dvhfset  41895  dvhset  41896  zndvdchrrhm  42781  aks4d1p1p6  42881  aks6d1c1  42924  aks6d1c5lem3  42945  sticksstones11  42964  fsuppssindlem2  43365  fsuppssind  43366  mzpclval  43497  mzpcompact2  43524  fsovrfovd  44776  supcnvlimsupmpt  46496  cncfshiftioo  46647  cncfiooicc  46649  dvsinax  46668  iblspltprt  46728  itgspltprt  46734  itgiccshift  46735  dirkercncflem2  46859  fourierdlem90  46951  fourierdlem92  46953  sge0val  47121  sge0prle  47156  sge0ss  47167  sge0iunmptlemfi  47168  sge0p1  47169  sge0iunmptlemre  47170  sge0iunmpt  47173  sge0xp  47184  ismeannd  47222  caratheodorylem1  47281  isomenndlem  47285  hoidmv1lelem2  47347  hoidmvlelem2  47351  hspmbllem2  47382  smflimsuplem1  47575  smflimsuplem4  47578  smflimsuplem7  47581  smflimsup  47583  mgpsumunsn  49182  lmod1zr  49314  iinfssclem1  49873  dfswapf2  50080  swapfval  50081  swapf2vala  50089  swapf2f1o  50095  swapf2f1oaALT  50097  prcofpropd  50198  prcof2a  50208  prcof2  50209  lmdfval  50468  cmdfval  50469