Theorem mpteq1d 5188

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

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

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-mpt 5180

This theorem is referenced by:  csbmpt2  5506  mptimass  6032  fmptapd  7117  offval  7631  mposn  8045  offsplitfpar  8061  mpocurryd  8211  cantnff  9583  dfac12lem1  10054  ackbij2lem2  10149  swrd00  14568  swrdlend  14577  swrd0  14582  repswswrd  14707  repswrevw  14710  revco  14757  ccatco  14758  ofccat  14892  vdwapfval  16899  imasdsval  17436  mrcfval  17531  catidd  17603  curfpropd  18156  pwspjmhm  18755  grpinvfval  18908  grpinvfvalALT  18909  psgnfval  19429  psgnfvalfi  19442  odfval  19461  odfvalALT  19462  frgpup3lem  19706  gsum2d2  19903  gsumxp  19905  telgsumfzs  19918  dprd2d2  19975  srgbinom  20166  gsummgp0  20253  pwsco1rhm  20435  pwsco2rhm  20436  funcrngcsetc  20573  funcrngcsetcALT  20574  funcringcsetc  20607  staffval  20774  freshmansdream  21529  phlpropd  21610  pjfval  21661  asclfval  21834  asclpropd  21853  mpfrcl  22040  evlsval  22041  psdffval  22100  evls1rhmlem  22265  evl1fval  22272  mvmulfval  22486  submafval  22523  mdetfval  22530  nfimdetndef  22533  mdetfval1  22534  mdet0pr  22536  m1detdiag  22541  madufval  22581  minmar1fval  22590  gsummatr01  22603  pmatcollpw3fi1lem2  22731  pmatcollpw3fi1  22732  cpmadugsumlemF  22820  ispnrm  23283  ptval2  23545  ptpjcn  23555  xkoptsub  23598  kqval  23670  pt1hmeo  23750  fmval  23887  tmdgsum  24039  subgtgp  24049  prdstmdd  24068  prdsxmslem2  24473  nmfval  24532  lebnumlem1  24916  limcmpt2  25841  dvcmulf  25904  mdegfval  26023  ulmshft  26355  wwlksnextbij  29975  off2  32719  of0r  32758  mptiffisupp  32772  mptprop  32777  fmptunsnop  32779  gsummpt2co  33131  gsumhashmul  33150  gsummulsubdishift1  33151  gsumwrd2dccat  33160  elrgspnlem4  33327  elrspunidl  33509  evl1deg2  33658  ply1coedeg  33670  gsummoncoe1fz  33679  splyval  33717  vietalem  33735  vieta  33736  algextdeglem4  33877  esumnul  34205  ofcfval4  34262  measdivcst  34381  omsfval  34451  signstfval  34721  signstf0  34725  signstfvn  34726  mrsubffval  35701  mrsubfval  35702  msubfval  35718  elmsubrn  35722  mvhfval  35727  msrfval  35731  fwddifval  36356  tailfval  36566  curf  37795  poimirlem24  37841  ftc1anc  37898  sdclem2  37939  erngfset  41055  erngfset-rN  41063  dvhfset  41336  dvhset  41337  zndvdchrrhm  42222  aks4d1p1p6  42323  aks6d1c1  42366  aks6d1c5lem3  42387  sticksstones11  42406  fsuppssindlem2  42831  fsuppssind  42832  mzpclval  42963  mzpcompact2  42990  fsovrfovd  44246  supcnvlimsupmpt  45981  cncfshiftioo  46132  cncfiooicc  46134  dvsinax  46153  iblspltprt  46213  itgspltprt  46219  itgiccshift  46220  dirkercncflem2  46344  fourierdlem90  46436  fourierdlem92  46438  sge0val  46606  sge0prle  46641  sge0ss  46652  sge0iunmptlemfi  46653  sge0p1  46654  sge0iunmptlemre  46655  sge0iunmpt  46658  sge0xp  46669  ismeannd  46707  caratheodorylem1  46766  isomenndlem  46770  hoidmv1lelem2  46832  hoidmvlelem2  46836  hspmbllem2  46867  smflimsuplem1  47060  smflimsuplem4  47063  smflimsuplem7  47066  smflimsup  47068  mgpsumunsn  48603  lmod1zr  48735  iinfssclem1  49295  dfswapf2  49502  swapfval  49503  swapf2vala  49511  swapf2f1o  49517  swapf2f1oaALT  49519  prcofpropd  49620  prcof2a  49630  prcof2  49631  lmdfval  49890  cmdfval  49891