Theorem mpteq1d 5194

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 5193	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ↦ cmpt 5185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5167  df-mpt 5186

This theorem is used by:  csbmpt2  5532  mptimass  6070  fmptapd  7176  offval  7702  mposn  8116  offsplitfpar  8132  mpocurryd  8289  curf  8893  cantnff  9678  dfac12lem1  10225  ackbij2lem2  10320  swrd00  14796  swrdlend  14807  swrd0  14812  repswswrd  14939  repswrevw  14942  revco  14989  ccatco  14990  ofccat  15127  vdwapfval  17154  imasdsval  17692  mrcfval  17787  catidd  17859  curfpropd  18412  pwspjmhm  19031  grpinvfval  19194  grpinvfvalALT  19195  psgnfval  19719  psgnfvalfi  19732  odfval  19751  odfvalALT  19752  frgpup3lem  19996  gsum2d2  20193  gsumxp  20195  telgsumfzs  20208  dprd2d2  20265  srgbinom  20462  gsummgp0  20552  pwsco1rhm  20746  pwsco2rhm  20747  funcrngcsetc  20897  funcrngcsetcALT  20898  funcringcsetc  20931  staffval  21103  freshmansdream  21885  phlpropd  21966  pjfval  22017  asclfval  22191  asclpropd  22210  mpfrcl  22399  evlsval  22400  psdffval  22483  evls1rhmlem  22644  evl1fval  22651  mvmulfval  22862  submafval  22899  mdetfval  22906  nfimdetndef  22909  mdetfval1  22910  mdet0pr  22912  m1detdiag  22917  madufval  22957  minmar1fval  22966  gsummatr01  22979  pmatcollpw3fi1lem2  23110  pmatcollpw3fi1  23111  cpmadugsumlemF  23199  ispnrm  23662  ptval2  23925  ptpjcn  23935  xkoptsub  23978  kqval  24050  pt1hmeo  24130  fmval  24267  tmdgsum  24419  subgtgp  24429  prdstmdd  24448  prdsxmslem2  24853  nmfval  24912  lebnumlem1  25287  limcmpt2  26209  dvcmulf  26270  mdegfval  26385  ulmshft  26722  wwlksnextbij  30496  off2  33282  of0r  33320  mptiffisupp  33333  mptprop  33338  fmptunsnop  33340  gsummpt2co  33655  gsumhashmul  33674  gsummulsubdishift1  33675  gsumwrd2dccat  33685  elrgspnlem4  33852  elrspunidl  34024  evl1deg2  34155  ply1coedeg  34167  gsummoncoe1fz  34176  0mplrim  34192  splyval  34237  vietalem  34257  vieta  34258  algextdeglem4  34398  esumnul  34726  ofcfval4  34783  measdivcst  34903  omsfval  34972  signstfval  35239  signstf0  35243  signstfvn  35244  mrsubffval  36358  mrsubfval  36359  msubfval  36375  elmsubrn  36379  mvhfval  36384  msrfval  36388  fwddifval  37019  tailfval  37252  poimirlem24  38655  ftc1anc  38712  sdclem2  38769  erngfset  41949  erngfset-rN  41957  dvhfset  42230  dvhset  42231  zndvdchrrhm  43116  aks4d1p1p6  43216  aks6d1c1  43259  aks6d1c5lem3  43280  sticksstones11  43299  fsuppssindlem2  43713  fsuppssind  43714  mzpclval  43829  mzpcompact2  43856  fsovrfovd  45102  supcnvlimsupmpt  46844  cncfshiftioo  46995  cncfiooicc  46997  dvsinax  47016  iblspltprt  47076  itgspltprt  47082  itgiccshift  47083  dirkercncflem2  47207  fourierdlem90  47299  fourierdlem92  47301  sge0val  47469  sge0prle  47504  sge0ss  47515  sge0iunmptlemfi  47516  sge0p1  47517  sge0iunmptlemre  47518  sge0iunmpt  47521  sge0xp  47532  ismeannd  47570  caratheodorylem1  47629  isomenndlem  47633  hoidmv1lelem2  47695  hoidmvlelem2  47699  hspmbllem2  47730  smflimsuplem1  47923  smflimsuplem4  47926  smflimsuplem7  47929  smflimsup  47931  mgpsumunsn  49566  lmod1zr  49698  ovmpomptd  50075  iinfssclem1  50261  dfswapf2  50476  swapfval  50477  swapf2vala  50485  swapf2f1o  50491  swapf2f1oaALT  50493  prcofpropd  50607  prcof2a  50617  prcof2  50618  lmdfval  50925  cmdfval  50926