Theorem mpteq1d 5176

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

Syntax hints:   → wi 4   = wceq 1542   ↦ cmpt 5167

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5149  df-mpt 5168

This theorem is referenced by:  csbmpt2  5506  mptimass  6032  fmptapd  7119  offval  7633  mposn  8046  offsplitfpar  8062  mpocurryd  8212  cantnff  9586  dfac12lem1  10057  ackbij2lem2  10152  swrd00  14598  swrdlend  14607  swrd0  14612  repswswrd  14737  repswrevw  14740  revco  14787  ccatco  14788  ofccat  14922  vdwapfval  16933  imasdsval  17470  mrcfval  17565  catidd  17637  curfpropd  18190  pwspjmhm  18789  grpinvfval  18945  grpinvfvalALT  18946  psgnfval  19466  psgnfvalfi  19479  odfval  19498  odfvalALT  19499  frgpup3lem  19743  gsum2d2  19940  gsumxp  19942  telgsumfzs  19955  dprd2d2  20012  srgbinom  20203  gsummgp0  20288  pwsco1rhm  20470  pwsco2rhm  20471  funcrngcsetc  20608  funcrngcsetcALT  20609  funcringcsetc  20642  staffval  20809  freshmansdream  21564  phlpropd  21645  pjfval  21696  asclfval  21868  asclpropd  21887  mpfrcl  22073  evlsval  22074  psdffval  22133  evls1rhmlem  22296  evl1fval  22303  mvmulfval  22517  submafval  22554  mdetfval  22561  nfimdetndef  22564  mdetfval1  22565  mdet0pr  22567  m1detdiag  22572  madufval  22612  minmar1fval  22621  gsummatr01  22634  pmatcollpw3fi1lem2  22762  pmatcollpw3fi1  22763  cpmadugsumlemF  22851  ispnrm  23314  ptval2  23576  ptpjcn  23586  xkoptsub  23629  kqval  23701  pt1hmeo  23781  fmval  23918  tmdgsum  24070  subgtgp  24080  prdstmdd  24099  prdsxmslem2  24504  nmfval  24563  lebnumlem1  24938  limcmpt2  25861  dvcmulf  25922  mdegfval  26037  ulmshft  26368  wwlksnextbij  29985  off2  32729  of0r  32767  mptiffisupp  32781  mptprop  32786  fmptunsnop  32788  gsummpt2co  33124  gsumhashmul  33143  gsummulsubdishift1  33144  gsumwrd2dccat  33154  elrgspnlem4  33321  elrspunidl  33503  evl1deg2  33652  ply1coedeg  33664  gsummoncoe1fz  33673  splyval  33718  vietalem  33738  vieta  33739  algextdeglem4  33880  esumnul  34208  ofcfval4  34265  measdivcst  34384  omsfval  34454  signstfval  34724  signstf0  34728  signstfvn  34729  mrsubffval  35705  mrsubfval  35706  msubfval  35722  elmsubrn  35726  mvhfval  35731  msrfval  35735  fwddifval  36360  tailfval  36570  curf  37933  poimirlem24  37979  ftc1anc  38036  sdclem2  38077  erngfset  41259  erngfset-rN  41267  dvhfset  41540  dvhset  41541  zndvdchrrhm  42426  aks4d1p1p6  42526  aks6d1c1  42569  aks6d1c5lem3  42590  sticksstones11  42609  fsuppssindlem2  43039  fsuppssind  43040  mzpclval  43171  mzpcompact2  43198  fsovrfovd  44454  supcnvlimsupmpt  46187  cncfshiftioo  46338  cncfiooicc  46340  dvsinax  46359  iblspltprt  46419  itgspltprt  46425  itgiccshift  46426  dirkercncflem2  46550  fourierdlem90  46642  fourierdlem92  46644  sge0val  46812  sge0prle  46847  sge0ss  46858  sge0iunmptlemfi  46859  sge0p1  46860  sge0iunmptlemre  46861  sge0iunmpt  46864  sge0xp  46875  ismeannd  46913  caratheodorylem1  46972  isomenndlem  46976  hoidmv1lelem2  47038  hoidmvlelem2  47042  hspmbllem2  47073  smflimsuplem1  47266  smflimsuplem4  47269  smflimsuplem7  47272  smflimsup  47274  mgpsumunsn  48849  lmod1zr  48981  iinfssclem1  49541  dfswapf2  49748  swapfval  49749  swapf2vala  49757  swapf2f1o  49763  swapf2f1oaALT  49765  prcofpropd  49866  prcof2a  49876  prcof2  49877  lmdfval  50136  cmdfval  50137