Theorem mpteq1d 5189

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

Syntax hints:   → wi 4   = wceq 1559   ↦ cmpt 5180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5162  df-mpt 5181

This theorem is referenced by:  csbmpt2  5527  mptimass  6059  fmptapd  7151  offval  7665  mposn  8077  offsplitfpar  8093  mpocurryd  8244  cantnff  9626  dfac12lem1  10097  ackbij2lem2  10192  swrd00  14655  swrdlend  14664  swrd0  14669  repswswrd  14794  repswrevw  14797  revco  14844  ccatco  14845  ofccat  14979  vdwapfval  16990  imasdsval  17528  mrcfval  17623  catidd  17695  curfpropd  18248  pwspjmhm  18847  grpinvfval  19003  grpinvfvalALT  19004  psgnfval  19523  psgnfvalfi  19536  odfval  19555  odfvalALT  19556  frgpup3lem  19800  gsum2d2  19997  gsumxp  19999  telgsumfzs  20012  dprd2d2  20069  srgbinom  20260  gsummgp0  20345  pwsco1rhm  20530  pwsco2rhm  20531  funcrngcsetc  20669  funcrngcsetcALT  20670  funcringcsetc  20703  staffval  20870  freshmansdream  21606  phlpropd  21687  pjfval  21738  asclfval  21910  asclpropd  21929  mpfrcl  22118  evlsval  22119  psdffval  22202  evls1rhmlem  22364  evl1fval  22371  mvmulfval  22582  submafval  22619  mdetfval  22626  nfimdetndef  22629  mdetfval1  22630  mdet0pr  22632  m1detdiag  22637  madufval  22677  minmar1fval  22686  gsummatr01  22699  pmatcollpw3fi1lem2  22827  pmatcollpw3fi1  22828  cpmadugsumlemF  22916  ispnrm  23379  ptval2  23641  ptpjcn  23651  xkoptsub  23694  kqval  23766  pt1hmeo  23846  fmval  23983  tmdgsum  24135  subgtgp  24145  prdstmdd  24164  prdsxmslem2  24569  nmfval  24628  lebnumlem1  25003  limcmpt2  25926  dvcmulf  25987  mdegfval  26102  ulmshft  26430  wwlksnextbij  30048  off2  32793  of0r  32831  mptiffisupp  32845  mptprop  32850  fmptunsnop  32852  gsummpt2co  33189  gsumhashmul  33208  gsummulsubdishift1  33209  gsumwrd2dccat  33219  elrgspnlem4  33387  elrspunidl  33575  evl1deg2  33734  ply1coedeg  33746  gsummoncoe1fz  33755  0mplrim  33772  splyval  33817  vietalem  33837  vieta  33838  algextdeglem4  33978  esumnul  34306  ofcfval4  34363  measdivcst  34482  omsfval  34552  signstfval  34822  signstf0  34826  signstfvn  34827  mrsubffval  35821  mrsubfval  35822  msubfval  35838  elmsubrn  35842  mvhfval  35847  msrfval  35851  fwddifval  36476  tailfval  36696  curf  38061  poimirlem24  38107  ftc1anc  38164  sdclem2  38205  erngfset  41387  erngfset-rN  41395  dvhfset  41668  dvhset  41669  zndvdchrrhm  42554  aks4d1p1p6  42654  aks6d1c1  42697  aks6d1c5lem3  42718  sticksstones11  42737  fsuppssindlem2  43138  fsuppssind  43139  mzpclval  43270  mzpcompact2  43297  fsovrfovd  44549  supcnvlimsupmpt  46279  cncfshiftioo  46430  cncfiooicc  46432  dvsinax  46451  iblspltprt  46511  itgspltprt  46517  itgiccshift  46518  dirkercncflem2  46642  fourierdlem90  46734  fourierdlem92  46736  sge0val  46904  sge0prle  46939  sge0ss  46950  sge0iunmptlemfi  46951  sge0p1  46952  sge0iunmptlemre  46953  sge0iunmpt  46956  sge0xp  46967  ismeannd  47005  caratheodorylem1  47064  isomenndlem  47068  hoidmv1lelem2  47130  hoidmvlelem2  47134  hspmbllem2  47165  smflimsuplem1  47358  smflimsuplem4  47361  smflimsuplem7  47364  smflimsup  47366  mgpsumunsn  48947  lmod1zr  49079  iinfssclem1  49639  dfswapf2  49846  swapfval  49847  swapf2vala  49855  swapf2f1o  49861  swapf2f1oaALT  49863  prcofpropd  49964  prcof2a  49974  prcof2  49975  lmdfval  50234  cmdfval  50235