Theorem mpteq1d 5243

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

Syntax hints:   → wi 4   = wceq 1541   ↦ cmpt 5231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-opab 5211  df-mpt 5232

This theorem is referenced by:  csbmpt2  5558  mptimass  6072  fmptapd  7171  offval  7681  mposn  8091  offsplitfpar  8107  mpocurryd  8256  cantnff  9671  dfac12lem1  10140  ackbij2lem2  10237  swrd00  14598  swrdlend  14607  swrd0  14612  repswswrd  14738  repswrevw  14741  revco  14789  ccatco  14790  ofccat  14920  vdwapfval  16908  imasdsval  17465  mrcfval  17556  catidd  17628  curfpropd  18190  pwspjmhm  18747  grpinvfval  18899  grpinvfvalALT  18900  psgnfval  19409  psgnfvalfi  19422  odfval  19441  odfvalALT  19442  frgpup3lem  19686  gsum2d2  19883  gsumxp  19885  telgsumfzs  19898  dprd2d2  19955  srgbinom  20125  gsummgp0  20206  pwsco1rhm  20393  pwsco2rhm  20394  staffval  20598  phlpropd  21427  pjfval  21480  asclfval  21652  asclpropd  21670  mpfrcl  21867  evlsval  21868  evls1rhmlem  22060  evl1fval  22067  mvmulfval  22264  submafval  22301  mdetfval  22308  nfimdetndef  22311  mdetfval1  22312  mdet0pr  22314  m1detdiag  22319  madufval  22359  minmar1fval  22368  gsummatr01  22381  pmatcollpw3fi1lem2  22509  pmatcollpw3fi1  22510  cpmadugsumlemF  22598  ispnrm  23063  ptval2  23325  ptpjcn  23335  xkoptsub  23378  kqval  23450  pt1hmeo  23530  fmval  23667  tmdgsum  23819  subgtgp  23829  prdstmdd  23848  prdsxmslem2  24258  nmfval  24317  lebnumlem1  24701  limcmpt2  25625  dvcmulf  25686  mdegfval  25804  ulmshft  26126  wwlksnextbij  29411  off2  32121  mptiffisupp  32170  mptprop  32175  gsummpt2co  32458  gsumhashmul  32466  freshmansdream  32639  elrspunidl  32808  algextdeglem4  33053  esumnul  33332  ofcfval4  33389  measdivcst  33508  omsfval  33579  signstfval  33861  signstf0  33865  signstfvn  33866  mrsubffval  34784  mrsubfval  34785  msubfval  34801  elmsubrn  34805  mvhfval  34810  msrfval  34814  fwddifval  35426  tailfval  35560  curf  36769  poimirlem24  36815  ftc1anc  36872  sdclem2  36913  erngfset  39973  erngfset-rN  39981  dvhfset  40254  dvhset  40255  aks4d1p1p6  41244  sticksstones11  41278  fsuppssindlem2  41466  fsuppssind  41467  mzpclval  41765  mzpcompact2  41792  fsovrfovd  43062  supcnvlimsupmpt  44756  cncfshiftioo  44907  cncfiooicc  44909  dvsinax  44928  iblspltprt  44988  itgspltprt  44994  itgiccshift  44995  dirkercncflem2  45119  fourierdlem90  45211  fourierdlem92  45213  sge0val  45381  sge0prle  45416  sge0ss  45427  sge0iunmptlemfi  45428  sge0p1  45429  sge0iunmptlemre  45430  sge0iunmpt  45433  sge0xp  45444  ismeannd  45482  caratheodorylem1  45541  isomenndlem  45545  hoidmv1lelem2  45607  hoidmvlelem2  45611  hspmbllem2  45642  smflimsuplem1  45835  smflimsuplem4  45838  smflimsuplem7  45841  smflimsup  45843  funcrngcsetc  46985  funcrngcsetcALT  46986  funcringcsetc  47022  mgpsumunsn  47126  lmod1zr  47262