Theorem mpteq1d 5185

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5158  df-mpt 5177

This theorem is referenced by:  csbmpt2  5505  mptimass  6028  fmptapd  7111  offval  7626  mposn  8043  offsplitfpar  8059  mpocurryd  8209  cantnff  9589  dfac12lem1  10057  ackbij2lem2  10152  swrd00  14569  swrdlend  14578  swrd0  14583  repswswrd  14708  repswrevw  14711  revco  14759  ccatco  14760  ofccat  14894  vdwapfval  16901  imasdsval  17437  mrcfval  17532  catidd  17604  curfpropd  18157  pwspjmhm  18722  grpinvfval  18875  grpinvfvalALT  18876  psgnfval  19397  psgnfvalfi  19410  odfval  19429  odfvalALT  19430  frgpup3lem  19674  gsum2d2  19871  gsumxp  19873  telgsumfzs  19886  dprd2d2  19943  srgbinom  20134  gsummgp0  20221  pwsco1rhm  20405  pwsco2rhm  20406  funcrngcsetc  20543  funcrngcsetcALT  20544  funcringcsetc  20577  staffval  20744  freshmansdream  21499  phlpropd  21580  pjfval  21631  asclfval  21804  asclpropd  21822  mpfrcl  22008  evlsval  22009  psdffval  22060  evls1rhmlem  22224  evl1fval  22231  mvmulfval  22445  submafval  22482  mdetfval  22489  nfimdetndef  22492  mdetfval1  22493  mdet0pr  22495  m1detdiag  22500  madufval  22540  minmar1fval  22549  gsummatr01  22562  pmatcollpw3fi1lem2  22690  pmatcollpw3fi1  22691  cpmadugsumlemF  22779  ispnrm  23242  ptval2  23504  ptpjcn  23514  xkoptsub  23557  kqval  23629  pt1hmeo  23709  fmval  23846  tmdgsum  23998  subgtgp  24008  prdstmdd  24027  prdsxmslem2  24433  nmfval  24492  lebnumlem1  24876  limcmpt2  25801  dvcmulf  25864  mdegfval  25983  ulmshft  26315  wwlksnextbij  29865  off2  32598  of0r  32635  mptiffisupp  32649  mptprop  32654  fmptunsnop  32656  gsummpt2co  33014  gsumhashmul  33027  gsumwrd2dccat  33033  elrgspnlem4  33195  elrspunidl  33375  evl1deg2  33522  algextdeglem4  33686  esumnul  34014  ofcfval4  34071  measdivcst  34190  omsfval  34261  signstfval  34531  signstf0  34535  signstfvn  34536  mrsubffval  35479  mrsubfval  35480  msubfval  35496  elmsubrn  35500  mvhfval  35505  msrfval  35509  fwddifval  36135  tailfval  36345  curf  37577  poimirlem24  37623  ftc1anc  37680  sdclem2  37721  erngfset  40778  erngfset-rN  40786  dvhfset  41059  dvhset  41060  zndvdchrrhm  41945  aks4d1p1p6  42046  aks6d1c1  42089  aks6d1c5lem3  42110  sticksstones11  42129  fsuppssindlem2  42565  fsuppssind  42566  mzpclval  42698  mzpcompact2  42725  fsovrfovd  43982  supcnvlimsupmpt  45723  cncfshiftioo  45874  cncfiooicc  45876  dvsinax  45895  iblspltprt  45955  itgspltprt  45961  itgiccshift  45962  dirkercncflem2  46086  fourierdlem90  46178  fourierdlem92  46180  sge0val  46348  sge0prle  46383  sge0ss  46394  sge0iunmptlemfi  46395  sge0p1  46396  sge0iunmptlemre  46397  sge0iunmpt  46400  sge0xp  46411  ismeannd  46449  caratheodorylem1  46508  isomenndlem  46512  hoidmv1lelem2  46574  hoidmvlelem2  46578  hspmbllem2  46609  smflimsuplem1  46802  smflimsuplem4  46805  smflimsuplem7  46808  smflimsup  46810  mgpsumunsn  48346  lmod1zr  48479  iinfssclem1  49040  dfswapf2  49247  swapfval  49248  swapf2vala  49256  swapf2f1o  49262  swapf2f1oaALT  49264  prcofpropd  49365  prcof2a  49375  prcof2  49376  lmdfval  49635  cmdfval  49636