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 1540   ↦ cmpt 5231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-opab 5211  df-mpt 5232

This theorem is referenced by:  csbmpt2  5558  mptimass  6072  fmptapd  7171  offval  7683  mposn  8094  offsplitfpar  8110  mpocurryd  8260  cantnff  9675  dfac12lem1  10144  ackbij2lem2  10241  swrd00  14601  swrdlend  14610  swrd0  14615  repswswrd  14741  repswrevw  14744  revco  14792  ccatco  14793  ofccat  14923  vdwapfval  16911  imasdsval  17468  mrcfval  17559  catidd  17631  curfpropd  18196  pwspjmhm  18753  grpinvfval  18906  grpinvfvalALT  18907  psgnfval  19416  psgnfvalfi  19429  odfval  19448  odfvalALT  19449  frgpup3lem  19693  gsum2d2  19890  gsumxp  19892  telgsumfzs  19905  dprd2d2  19962  srgbinom  20132  gsummgp0  20213  pwsco1rhm  20400  pwsco2rhm  20401  funcrngcsetc  20532  funcrngcsetcALT  20533  funcringcsetc  20566  staffval  20686  phlpropd  21518  pjfval  21571  asclfval  21743  asclpropd  21761  mpfrcl  21959  evlsval  21960  psdffval  22009  evls1rhmlem  22160  evl1fval  22167  mvmulfval  22364  submafval  22401  mdetfval  22408  nfimdetndef  22411  mdetfval1  22412  mdet0pr  22414  m1detdiag  22419  madufval  22459  minmar1fval  22468  gsummatr01  22481  pmatcollpw3fi1lem2  22609  pmatcollpw3fi1  22610  cpmadugsumlemF  22698  ispnrm  23163  ptval2  23425  ptpjcn  23435  xkoptsub  23478  kqval  23550  pt1hmeo  23630  fmval  23767  tmdgsum  23919  subgtgp  23929  prdstmdd  23948  prdsxmslem2  24358  nmfval  24417  lebnumlem1  24807  limcmpt2  25733  dvcmulf  25796  mdegfval  25918  ulmshft  26241  wwlksnextbij  29590  off2  32300  mptiffisupp  32349  mptprop  32354  gsummpt2co  32637  gsumhashmul  32645  freshmansdream  32818  elrspunidl  32987  algextdeglem4  33232  esumnul  33511  ofcfval4  33568  measdivcst  33687  omsfval  33758  signstfval  34040  signstf0  34044  signstfvn  34045  mrsubffval  34963  mrsubfval  34964  msubfval  34980  elmsubrn  34984  mvhfval  34989  msrfval  34993  fwddifval  35605  tailfval  35723  curf  36932  poimirlem24  36978  ftc1anc  37035  sdclem2  37076  erngfset  40136  erngfset-rN  40144  dvhfset  40417  dvhset  40418  aks4d1p1p6  41407  sticksstones11  41441  fsuppssindlem2  41629  fsuppssind  41630  mzpclval  41928  mzpcompact2  41955  fsovrfovd  43225  supcnvlimsupmpt  44918  cncfshiftioo  45069  cncfiooicc  45071  dvsinax  45090  iblspltprt  45150  itgspltprt  45156  itgiccshift  45157  dirkercncflem2  45281  fourierdlem90  45373  fourierdlem92  45375  sge0val  45543  sge0prle  45578  sge0ss  45589  sge0iunmptlemfi  45590  sge0p1  45591  sge0iunmptlemre  45592  sge0iunmpt  45595  sge0xp  45606  ismeannd  45644  caratheodorylem1  45703  isomenndlem  45707  hoidmv1lelem2  45769  hoidmvlelem2  45773  hspmbllem2  45804  smflimsuplem1  45997  smflimsuplem4  46000  smflimsuplem7  46003  smflimsup  46005  mgpsumunsn  47202  lmod1zr  47338