Theorem mpteq1d 5205

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

Syntax hints:   → wi 4   = wceq 1541   ↦ cmpt 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-opab 5173  df-mpt 5194

This theorem is referenced by:  csbmpt2  5520  fmptapd  7122  offval  7631  mposn  8040  offsplitfpar  8056  mpocurryd  8205  cantnff  9619  dfac12lem1  10088  ackbij2lem2  10185  swrd00  14544  swrdlend  14553  swrd0  14558  repswswrd  14684  repswrevw  14687  revco  14735  ccatco  14736  ofccat  14866  vdwapfval  16854  imasdsval  17411  mrcfval  17502  catidd  17574  curfpropd  18136  pwspjmhm  18654  grpinvfval  18803  grpinvfvalALT  18804  psgnfval  19296  psgnfvalfi  19309  odfval  19328  odfvalALT  19329  frgpup3lem  19573  gsum2d2  19765  gsumxp  19767  telgsumfzs  19780  dprd2d2  19837  srgbinom  19976  gsummgp0  20046  pwsco1rhm  20188  pwsco2rhm  20189  staffval  20362  phlpropd  21096  pjfval  21149  asclfval  21319  asclpropd  21337  mpfrcl  21532  evlsval  21533  evls1rhmlem  21724  evl1fval  21731  mvmulfval  21928  submafval  21965  mdetfval  21972  nfimdetndef  21975  mdetfval1  21976  mdet0pr  21978  m1detdiag  21983  madufval  22023  minmar1fval  22032  gsummatr01  22045  pmatcollpw3fi1lem2  22173  pmatcollpw3fi1  22174  cpmadugsumlemF  22262  ispnrm  22727  ptval2  22989  ptpjcn  22999  xkoptsub  23042  kqval  23114  pt1hmeo  23194  fmval  23331  tmdgsum  23483  subgtgp  23493  prdstmdd  23512  prdsxmslem2  23922  nmfval  23981  lebnumlem1  24361  limcmpt2  25285  dvcmulf  25346  mdegfval  25464  ulmshft  25786  wwlksnextbij  28910  off2  31624  mptiffisupp  31675  mptprop  31680  gsummpt2co  31960  gsumhashmul  31968  freshmansdream  32137  elrspunidl  32279  esumnul  32736  ofcfval4  32793  measdivcst  32912  omsfval  32983  signstfval  33265  signstf0  33269  signstfvn  33270  mrsubffval  34188  mrsubfval  34189  msubfval  34205  elmsubrn  34209  mvhfval  34214  msrfval  34218  fwddifval  34823  tailfval  34920  curf  36129  poimirlem24  36175  ftc1anc  36232  sdclem2  36274  erngfset  39335  erngfset-rN  39343  dvhfset  39616  dvhset  39617  aks4d1p1p6  40603  sticksstones11  40637  fsuppssindlem2  40825  fsuppssind  40826  mzpclval  41106  mzpcompact2  41133  fsovrfovd  42403  mptima2  43594  supcnvlimsupmpt  44102  cncfshiftioo  44253  cncfiooicc  44255  dvsinax  44274  iblspltprt  44334  itgspltprt  44340  itgiccshift  44341  dirkercncflem2  44465  fourierdlem90  44557  fourierdlem92  44559  sge0val  44727  sge0prle  44762  sge0ss  44773  sge0iunmptlemfi  44774  sge0p1  44775  sge0iunmptlemre  44776  sge0iunmpt  44779  sge0xp  44790  ismeannd  44828  caratheodorylem1  44887  isomenndlem  44891  hoidmv1lelem2  44953  hoidmvlelem2  44957  hspmbllem2  44988  smflimsuplem1  45181  smflimsuplem4  45184  smflimsuplem7  45187  smflimsup  45189  funcrngcsetc  46416  funcrngcsetcALT  46417  funcringcsetc  46453  mgpsumunsn  46557  lmod1zr  46694