Theorem mpteq1d 5169

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

Syntax hints:   → wi 4   = wceq 1547   ↦ cmpt 5160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-opab 5142  df-mpt 5161

This theorem is referenced by:  csbmpt2  5507  mptimass  6032  fmptapd  7122  offval  7636  mposn  8049  offsplitfpar  8065  mpocurryd  8216  cantnff  9593  dfac12lem1  10064  ackbij2lem2  10159  swrd00  14605  swrdlend  14614  swrd0  14619  repswswrd  14744  repswrevw  14747  revco  14794  ccatco  14795  ofccat  14929  vdwapfval  16940  imasdsval  17477  mrcfval  17572  catidd  17644  curfpropd  18197  pwspjmhm  18796  grpinvfval  18952  grpinvfvalALT  18953  psgnfval  19473  psgnfvalfi  19486  odfval  19505  odfvalALT  19506  frgpup3lem  19750  gsum2d2  19947  gsumxp  19949  telgsumfzs  19962  dprd2d2  20019  srgbinom  20210  gsummgp0  20295  pwsco1rhm  20480  pwsco2rhm  20481  funcrngcsetc  20619  funcrngcsetcALT  20620  funcringcsetc  20653  staffval  20820  freshmansdream  21556  phlpropd  21637  pjfval  21688  asclfval  21860  asclpropd  21879  mpfrcl  22068  evlsval  22069  psdffval  22152  evls1rhmlem  22314  evl1fval  22321  mvmulfval  22532  submafval  22569  mdetfval  22576  nfimdetndef  22579  mdetfval1  22580  mdet0pr  22582  m1detdiag  22587  madufval  22627  minmar1fval  22636  gsummatr01  22649  pmatcollpw3fi1lem2  22777  pmatcollpw3fi1  22778  cpmadugsumlemF  22866  ispnrm  23329  ptval2  23591  ptpjcn  23601  xkoptsub  23644  kqval  23716  pt1hmeo  23796  fmval  23933  tmdgsum  24085  subgtgp  24095  prdstmdd  24114  prdsxmslem2  24519  nmfval  24578  lebnumlem1  24953  limcmpt2  25876  dvcmulf  25937  mdegfval  26052  ulmshft  26380  wwlksnextbij  29995  off2  32740  of0r  32778  mptiffisupp  32792  mptprop  32797  fmptunsnop  32799  gsummpt2co  33136  gsumhashmul  33155  gsummulsubdishift1  33156  gsumwrd2dccat  33166  elrgspnlem4  33333  elrspunidl  33518  evl1deg2  33667  ply1coedeg  33679  gsummoncoe1fz  33688  0mplrim  33705  splyval  33750  vietalem  33770  vieta  33771  algextdeglem4  33911  esumnul  34239  ofcfval4  34296  measdivcst  34415  omsfval  34485  signstfval  34755  signstf0  34759  signstfvn  34760  mrsubffval  35742  mrsubfval  35743  msubfval  35759  elmsubrn  35763  mvhfval  35768  msrfval  35772  fwddifval  36397  tailfval  36607  curf  37972  poimirlem24  38018  ftc1anc  38075  sdclem2  38116  erngfset  41298  erngfset-rN  41306  dvhfset  41579  dvhset  41580  zndvdchrrhm  42465  aks4d1p1p6  42565  aks6d1c1  42608  aks6d1c5lem3  42629  sticksstones11  42648  fsuppssindlem2  43049  fsuppssind  43050  mzpclval  43181  mzpcompact2  43208  fsovrfovd  44460  supcnvlimsupmpt  46191  cncfshiftioo  46342  cncfiooicc  46344  dvsinax  46363  iblspltprt  46423  itgspltprt  46429  itgiccshift  46430  dirkercncflem2  46554  fourierdlem90  46646  fourierdlem92  46648  sge0val  46816  sge0prle  46851  sge0ss  46862  sge0iunmptlemfi  46863  sge0p1  46864  sge0iunmptlemre  46865  sge0iunmpt  46868  sge0xp  46879  ismeannd  46917  caratheodorylem1  46976  isomenndlem  46980  hoidmv1lelem2  47042  hoidmvlelem2  47046  hspmbllem2  47077  smflimsuplem1  47270  smflimsuplem4  47273  smflimsuplem7  47276  smflimsup  47278  mgpsumunsn  48859  lmod1zr  48991  iinfssclem1  49551  dfswapf2  49758  swapfval  49759  swapf2vala  49767  swapf2f1o  49773  swapf2f1oaALT  49775  prcofpropd  49876  prcof2a  49886  prcof2  49887  lmdfval  50146  cmdfval  50147