Theorem mpteq1d 5195

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

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-mpt 5187

This theorem is used by:  csbmpt2  5533  mptimass  6067  fmptapd  7168  offval  7691  mposn  8103  offsplitfpar  8119  mpocurryd  8270  curf  8874  cantnff  9659  dfac12lem1  10203  ackbij2lem2  10298  swrd00  14772  swrdlend  14783  swrd0  14788  repswswrd  14915  repswrevw  14918  revco  14965  ccatco  14966  ofccat  15102  vdwapfval  17129  imasdsval  17667  mrcfval  17762  catidd  17834  curfpropd  18387  pwspjmhm  19006  grpinvfval  19169  grpinvfvalALT  19170  psgnfval  19694  psgnfvalfi  19707  odfval  19726  odfvalALT  19727  frgpup3lem  19971  gsum2d2  20168  gsumxp  20170  telgsumfzs  20183  dprd2d2  20240  srgbinom  20437  gsummgp0  20527  pwsco1rhm  20721  pwsco2rhm  20722  funcrngcsetc  20872  funcrngcsetcALT  20873  funcringcsetc  20906  staffval  21078  freshmansdream  21860  phlpropd  21941  pjfval  21992  asclfval  22166  asclpropd  22185  mpfrcl  22374  evlsval  22375  psdffval  22458  evls1rhmlem  22619  evl1fval  22626  mvmulfval  22837  submafval  22874  mdetfval  22881  nfimdetndef  22884  mdetfval1  22885  mdet0pr  22887  m1detdiag  22892  madufval  22932  minmar1fval  22941  gsummatr01  22954  pmatcollpw3fi1lem2  23085  pmatcollpw3fi1  23086  cpmadugsumlemF  23174  ispnrm  23637  ptval2  23900  ptpjcn  23910  xkoptsub  23953  kqval  24025  pt1hmeo  24105  fmval  24242  tmdgsum  24394  subgtgp  24404  prdstmdd  24423  prdsxmslem2  24828  nmfval  24887  lebnumlem1  25262  limcmpt2  26184  dvcmulf  26245  mdegfval  26360  ulmshft  26699  wwlksnextbij  30473  off2  33217  of0r  33255  mptiffisupp  33268  mptprop  33273  fmptunsnop  33275  gsummpt2co  33591  gsumhashmul  33610  gsummulsubdishift1  33611  gsumwrd2dccat  33621  elrgspnlem4  33788  elrspunidl  33960  evl1deg2  34091  ply1coedeg  34103  gsummoncoe1fz  34112  0mplrim  34128  splyval  34173  vietalem  34193  vieta  34194  algextdeglem4  34334  esumnul  34662  ofcfval4  34719  measdivcst  34839  omsfval  34909  signstfval  35176  signstf0  35180  signstfvn  35181  mrsubffval  36241  mrsubfval  36242  msubfval  36258  elmsubrn  36262  mvhfval  36267  msrfval  36271  fwddifval  36897  tailfval  37130  poimirlem24  38530  ftc1anc  38587  sdclem2  38644  erngfset  41824  erngfset-rN  41832  dvhfset  42105  dvhset  42106  zndvdchrrhm  42991  aks4d1p1p6  43091  aks6d1c1  43134  aks6d1c5lem3  43155  sticksstones11  43174  fsuppssindlem2  43582  fsuppssind  43583  mzpclval  43689  mzpcompact2  43716  fsovrfovd  44968  supcnvlimsupmpt  46695  cncfshiftioo  46846  cncfiooicc  46848  dvsinax  46867  iblspltprt  46927  itgspltprt  46933  itgiccshift  46934  dirkercncflem2  47058  fourierdlem90  47150  fourierdlem92  47152  sge0val  47320  sge0prle  47355  sge0ss  47366  sge0iunmptlemfi  47367  sge0p1  47368  sge0iunmptlemre  47369  sge0iunmpt  47372  sge0xp  47383  ismeannd  47421  caratheodorylem1  47480  isomenndlem  47484  hoidmv1lelem2  47546  hoidmvlelem2  47550  hspmbllem2  47581  smflimsuplem1  47774  smflimsuplem4  47777  smflimsuplem7  47780  smflimsup  47782  mgpsumunsn  49417  lmod1zr  49549  iinfssclem1  50106  dfswapf2  50313  swapfval  50314  swapf2vala  50322  swapf2f1o  50328  swapf2f1oaALT  50330  prcofpropd  50431  prcof2a  50441  prcof2  50442  lmdfval  50701  cmdfval  50702