Theorem mpteq1d 5210

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

Syntax hints:   → wi 4   = wceq 1540   ↦ cmpt 5201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-opab 5182  df-mpt 5202

This theorem is referenced by:  csbmpt2  5533  mptimass  6060  fmptapd  7162  offval  7678  mposn  8100  offsplitfpar  8116  mpocurryd  8266  cantnff  9686  dfac12lem1  10156  ackbij2lem2  10251  swrd00  14660  swrdlend  14669  swrd0  14674  repswswrd  14800  repswrevw  14803  revco  14851  ccatco  14852  ofccat  14986  vdwapfval  16989  imasdsval  17527  mrcfval  17618  catidd  17690  curfpropd  18243  pwspjmhm  18806  grpinvfval  18959  grpinvfvalALT  18960  psgnfval  19479  psgnfvalfi  19492  odfval  19511  odfvalALT  19512  frgpup3lem  19756  gsum2d2  19953  gsumxp  19955  telgsumfzs  19968  dprd2d2  20025  srgbinom  20189  gsummgp0  20276  pwsco1rhm  20460  pwsco2rhm  20461  funcrngcsetc  20598  funcrngcsetcALT  20599  funcringcsetc  20632  staffval  20799  freshmansdream  21533  phlpropd  21613  pjfval  21664  asclfval  21837  asclpropd  21855  mpfrcl  22041  evlsval  22042  psdffval  22093  evls1rhmlem  22257  evl1fval  22264  mvmulfval  22478  submafval  22515  mdetfval  22522  nfimdetndef  22525  mdetfval1  22526  mdet0pr  22528  m1detdiag  22533  madufval  22573  minmar1fval  22582  gsummatr01  22595  pmatcollpw3fi1lem2  22723  pmatcollpw3fi1  22724  cpmadugsumlemF  22812  ispnrm  23275  ptval2  23537  ptpjcn  23547  xkoptsub  23590  kqval  23662  pt1hmeo  23742  fmval  23879  tmdgsum  24031  subgtgp  24041  prdstmdd  24060  prdsxmslem2  24466  nmfval  24525  lebnumlem1  24909  limcmpt2  25835  dvcmulf  25898  mdegfval  26017  ulmshft  26349  wwlksnextbij  29830  off2  32565  of0r  32602  mptiffisupp  32616  mptprop  32621  fmptunsnop  32623  gsummpt2co  32988  gsumhashmul  33001  gsumwrd2dccat  33007  elrgspnlem4  33186  elrspunidl  33389  evl1deg2  33536  algextdeglem4  33700  esumnul  34025  ofcfval4  34082  measdivcst  34201  omsfval  34272  signstfval  34542  signstf0  34546  signstfvn  34547  mrsubffval  35475  mrsubfval  35476  msubfval  35492  elmsubrn  35496  mvhfval  35501  msrfval  35505  fwddifval  36126  tailfval  36336  curf  37568  poimirlem24  37614  ftc1anc  37671  sdclem2  37712  erngfset  40764  erngfset-rN  40772  dvhfset  41045  dvhset  41046  zndvdchrrhm  41931  aks4d1p1p6  42032  aks6d1c1  42075  aks6d1c5lem3  42096  sticksstones11  42115  fsuppssindlem2  42562  fsuppssind  42563  mzpclval  42695  mzpcompact2  42722  fsovrfovd  43980  supcnvlimsupmpt  45718  cncfshiftioo  45869  cncfiooicc  45871  dvsinax  45890  iblspltprt  45950  itgspltprt  45956  itgiccshift  45957  dirkercncflem2  46081  fourierdlem90  46173  fourierdlem92  46175  sge0val  46343  sge0prle  46378  sge0ss  46389  sge0iunmptlemfi  46390  sge0p1  46391  sge0iunmptlemre  46392  sge0iunmpt  46395  sge0xp  46406  ismeannd  46444  caratheodorylem1  46503  isomenndlem  46507  hoidmv1lelem2  46569  hoidmvlelem2  46573  hspmbllem2  46604  smflimsuplem1  46797  smflimsuplem4  46800  smflimsuplem7  46803  smflimsup  46805  mgpsumunsn  48284  lmod1zr  48417  iinfssclem1  48969  dfswapf2  49126  swapfval  49127  swapf2vala  49135  swapf2f1o  49141  swapf2f1oaALT  49143  prcof2a  49247  prcof2  49248  lmdfval  49471  cmdfval  49472