Theorem mpteq1d 5199

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ↦ cmpt 5190

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5172  df-mpt 5191

This theorem is used by:  csbmpt2  5538  mptimass  6084  fmptapd  7202  offval  7729  mposn  8144  offsplitfpar  8160  mpocurryd  8317  curf  8921  cantnff  9705  dfac12lem1  10252  ackbij2lem2  10347  swrd00  14823  swrdlend  14834  swrd0  14839  repswswrd  14966  repswrevw  14969  revco  15016  ccatco  15017  ofccat  15154  vdwapfval  17181  imasdsval  17719  mrcfval  17814  catidd  17886  curfpropd  18439  pwspjmhm  19058  grpinvfval  19221  grpinvfvalALT  19222  psgnfval  19747  psgnfvalfi  19760  odfval  19779  odfvalALT  19780  frgpup3lem  20024  gsum2d2  20221  gsumxp  20223  telgsumfzs  20236  dprd2d2  20293  srgbinom  20490  gsummgp0  20580  pwsco1rhm  20774  pwsco2rhm  20775  funcrngcsetc  20925  funcrngcsetcALT  20926  funcringcsetc  20959  staffval  21131  freshmansdream  21913  phlpropd  21994  pjfval  22045  asclfval  22219  asclpropd  22238  mpfrcl  22427  evlsval  22428  psdffval  22511  evls1rhmlem  22672  evl1fval  22679  mvmulfval  22890  submafval  22927  mdetfval  22934  nfimdetndef  22937  mdetfval1  22938  mdet0pr  22940  m1detdiag  22945  madufval  22985  minmar1fval  22994  gsummatr01  23007  pmatcollpw3fi1lem2  23138  pmatcollpw3fi1  23139  cpmadugsumlemF  23227  ispnrm  23690  ptval2  23953  ptpjcn  23963  xkoptsub  24006  kqval  24078  pt1hmeo  24158  fmval  24295  tmdgsum  24447  subgtgp  24457  prdstmdd  24476  prdsxmslem2  24881  nmfval  24940  lebnumlem1  25315  limcmpt2  26237  dvcmulf  26298  mdegfval  26413  ulmshft  26750  wwlksnextbij  30524  off2  33310  of0r  33347  mptiffisupp  33360  mptprop  33365  fmptunsnop  33367  gsummpt2co  33685  gsumhashmul  33704  gsummulsubdishift1  33705  gsumwrd2dccat  33715  elrgspnlem4  33882  elrspunidl  34062  evl1deg2  34192  ply1coedeg  34204  gsummoncoe1fz  34213  0mplrim  34229  splyval  34274  vietalem  34294  vieta  34295  algextdeglem4  34435  esumnul  34763  ofcfval4  34820  measdivcst  34940  omsfval  35009  signstfval  35276  signstf0  35280  signstfvn  35281  mrsubffval  36452  mrsubfval  36453  msubfval  36469  elmsubrn  36473  mvhfval  36478  msrfval  36482  fwddifval  37118  tailfval  37351  poimirlem24  38767  ftc1anc  38824  sdclem2  38879  erngfset  42059  erngfset-rN  42067  dvhfset  42340  dvhset  42341  zndvdchrrhm  43226  aks4d1p1p6  43326  aks6d1c1  43369  aks6d1c5lem3  43390  sticksstones11  43409  fsuppssindlem2  43824  fsuppssind  43825  mzpclval  43940  mzpcompact2  43967  fsovrfovd  45212  supcnvlimsupmpt  46966  cncfshiftioo  47117  cncfiooicc  47119  dvsinax  47138  iblspltprt  47198  itgspltprt  47204  itgiccshift  47205  dirkercncflem2  47329  fourierdlem90  47421  fourierdlem92  47423  sge0val  47591  sge0prle  47626  sge0ss  47637  sge0iunmptlemfi  47638  sge0p1  47639  sge0iunmptlemre  47640  sge0iunmpt  47643  sge0xp  47654  ismeannd  47692  caratheodorylem1  47751  isomenndlem  47755  hoidmv1lelem2  47817  hoidmvlelem2  47821  hspmbllem2  47852  smflimsuplem1  48045  smflimsuplem4  48048  smflimsuplem7  48051  smflimsup  48053  mgpsumunsn  49688  lmod1zr  49820  ovmpomptd  50197  iinfssclem1  50383  dfswapf2  50598  swapfval  50599  swapf2vala  50607  swapf2f1o  50613  swapf2f1oaALT  50615  prcofpropd  50729  prcof2a  50739  prcof2  50740  lmdfval  51047  cmdfval  51048