Theorem mpteq1d 5195

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

Syntax hints:   → wi 4   = wceq 1563   ↦ cmpt 5186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5168  df-mpt 5187

This theorem is referenced by:  csbmpt2  5534  mptimass  6066  fmptapd  7159  offval  7673  mposn  8086  offsplitfpar  8102  mpocurryd  8253  cantnff  9631  dfac12lem1  10115  ackbij2lem2  10210  swrd00  14672  swrdlend  14681  swrd0  14686  repswswrd  14811  repswrevw  14814  revco  14861  ccatco  14862  ofccat  14996  vdwapfval  17021  imasdsval  17559  mrcfval  17654  catidd  17726  curfpropd  18279  pwspjmhm  18879  grpinvfval  19035  grpinvfvalALT  19036  psgnfval  19561  psgnfvalfi  19574  odfval  19593  odfvalALT  19594  frgpup3lem  19838  gsum2d2  20035  gsumxp  20037  telgsumfzs  20050  dprd2d2  20107  srgbinom  20304  gsummgp0  20390  pwsco1rhm  20575  pwsco2rhm  20576  funcrngcsetc  20716  funcrngcsetcALT  20717  funcringcsetc  20750  staffval  20913  freshmansdream  21684  phlpropd  21765  pjfval  21816  asclfval  21988  asclpropd  22007  mpfrcl  22196  evlsval  22197  psdffval  22280  evls1rhmlem  22442  evl1fval  22449  mvmulfval  22660  submafval  22697  mdetfval  22704  nfimdetndef  22707  mdetfval1  22708  mdet0pr  22710  m1detdiag  22715  madufval  22755  minmar1fval  22764  gsummatr01  22777  pmatcollpw3fi1lem2  22905  pmatcollpw3fi1  22906  cpmadugsumlemF  22994  ispnrm  23457  ptval2  23719  ptpjcn  23729  xkoptsub  23772  kqval  23844  pt1hmeo  23924  fmval  24061  tmdgsum  24213  subgtgp  24223  prdstmdd  24242  prdsxmslem2  24647  nmfval  24706  lebnumlem1  25081  limcmpt2  26004  dvcmulf  26065  mdegfval  26180  ulmshft  26511  wwlksnextbij  30160  off2  32898  of0r  32936  mptiffisupp  32950  mptprop  32955  fmptunsnop  32957  gsummpt2co  33281  gsumhashmul  33300  gsummulsubdishift1  33301  gsumwrd2dccat  33311  elrgspnlem4  33478  elrspunidl  33652  evl1deg2  33784  ply1coedeg  33796  gsummoncoe1fz  33805  0mplrim  33821  splyval  33866  vietalem  33886  vieta  33887  algextdeglem4  34027  esumnul  34355  ofcfval4  34412  measdivcst  34531  omsfval  34601  signstfval  34868  signstf0  34872  signstfvn  34873  mrsubffval  35870  mrsubfval  35871  msubfval  35887  elmsubrn  35891  mvhfval  35896  msrfval  35900  fwddifval  36525  tailfval  36745  curf  38109  poimirlem24  38155  ftc1anc  38212  sdclem2  38253  erngfset  41435  erngfset-rN  41443  dvhfset  41716  dvhset  41717  zndvdchrrhm  42602  aks4d1p1p6  42702  aks6d1c1  42745  aks6d1c5lem3  42766  sticksstones11  42785  fsuppssindlem2  43186  fsuppssind  43187  mzpclval  43318  mzpcompact2  43345  fsovrfovd  44597  supcnvlimsupmpt  46313  cncfshiftioo  46464  cncfiooicc  46466  dvsinax  46485  iblspltprt  46545  itgspltprt  46551  itgiccshift  46552  dirkercncflem2  46676  fourierdlem90  46768  fourierdlem92  46770  sge0val  46938  sge0prle  46973  sge0ss  46984  sge0iunmptlemfi  46985  sge0p1  46986  sge0iunmptlemre  46987  sge0iunmpt  46990  sge0xp  47001  ismeannd  47039  caratheodorylem1  47098  isomenndlem  47102  hoidmv1lelem2  47164  hoidmvlelem2  47168  hspmbllem2  47199  smflimsuplem1  47392  smflimsuplem4  47395  smflimsuplem7  47398  smflimsup  47400  mgpsumunsn  48992  lmod1zr  49124  iinfssclem1  49683  dfswapf2  49890  swapfval  49891  swapf2vala  49899  swapf2f1o  49905  swapf2f1oaALT  49907  prcofpropd  50008  prcof2a  50018  prcof2  50019  lmdfval  50278  cmdfval  50279