Theorem mpteq1d 5237

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

Syntax hints:   → wi 4   = wceq 1540   ↦ cmpt 5225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-mpt 5226

This theorem is referenced by:  csbmpt2  5563  mptimass  6091  fmptapd  7191  offval  7706  mposn  8128  offsplitfpar  8144  mpocurryd  8294  cantnff  9714  dfac12lem1  10184  ackbij2lem2  10279  swrd00  14682  swrdlend  14691  swrd0  14696  repswswrd  14822  repswrevw  14825  revco  14873  ccatco  14874  ofccat  15008  vdwapfval  17009  imasdsval  17560  mrcfval  17651  catidd  17723  curfpropd  18278  pwspjmhm  18843  grpinvfval  18996  grpinvfvalALT  18997  psgnfval  19518  psgnfvalfi  19531  odfval  19550  odfvalALT  19551  frgpup3lem  19795  gsum2d2  19992  gsumxp  19994  telgsumfzs  20007  dprd2d2  20064  srgbinom  20228  gsummgp0  20315  pwsco1rhm  20502  pwsco2rhm  20503  funcrngcsetc  20640  funcrngcsetcALT  20641  funcringcsetc  20674  staffval  20842  freshmansdream  21593  phlpropd  21673  pjfval  21726  asclfval  21899  asclpropd  21917  mpfrcl  22109  evlsval  22110  psdffval  22161  evls1rhmlem  22325  evl1fval  22332  mvmulfval  22548  submafval  22585  mdetfval  22592  nfimdetndef  22595  mdetfval1  22596  mdet0pr  22598  m1detdiag  22603  madufval  22643  minmar1fval  22652  gsummatr01  22665  pmatcollpw3fi1lem2  22793  pmatcollpw3fi1  22794  cpmadugsumlemF  22882  ispnrm  23347  ptval2  23609  ptpjcn  23619  xkoptsub  23662  kqval  23734  pt1hmeo  23814  fmval  23951  tmdgsum  24103  subgtgp  24113  prdstmdd  24132  prdsxmslem2  24542  nmfval  24601  lebnumlem1  24993  limcmpt2  25919  dvcmulf  25982  mdegfval  26101  ulmshft  26433  wwlksnextbij  29922  off2  32651  of0r  32688  mptiffisupp  32702  mptprop  32707  fmptunsnop  32709  gsummpt2co  33051  gsumhashmul  33064  gsumwrd2dccat  33070  elrgspnlem4  33249  elrspunidl  33456  evl1deg2  33602  algextdeglem4  33761  esumnul  34049  ofcfval4  34106  measdivcst  34225  omsfval  34296  signstfval  34579  signstf0  34583  signstfvn  34584  mrsubffval  35512  mrsubfval  35513  msubfval  35529  elmsubrn  35533  mvhfval  35538  msrfval  35542  fwddifval  36163  tailfval  36373  curf  37605  poimirlem24  37651  ftc1anc  37708  sdclem2  37749  erngfset  40801  erngfset-rN  40809  dvhfset  41082  dvhset  41083  zndvdchrrhm  41972  aks4d1p1p6  42074  aks6d1c1  42117  aks6d1c5lem3  42138  sticksstones11  42157  fsuppssindlem2  42602  fsuppssind  42603  mzpclval  42736  mzpcompact2  42763  fsovrfovd  44022  supcnvlimsupmpt  45756  cncfshiftioo  45907  cncfiooicc  45909  dvsinax  45928  iblspltprt  45988  itgspltprt  45994  itgiccshift  45995  dirkercncflem2  46119  fourierdlem90  46211  fourierdlem92  46213  sge0val  46381  sge0prle  46416  sge0ss  46427  sge0iunmptlemfi  46428  sge0p1  46429  sge0iunmptlemre  46430  sge0iunmpt  46433  sge0xp  46444  ismeannd  46482  caratheodorylem1  46541  isomenndlem  46545  hoidmv1lelem2  46607  hoidmvlelem2  46611  hspmbllem2  46642  smflimsuplem1  46835  smflimsuplem4  46838  smflimsuplem7  46841  smflimsup  46843  mgpsumunsn  48277  lmod1zr  48410  dfswapf2  48967  swapfval  48968  swapf2vala  48976  swapf2f1o  48982  swapf2f1oaALT  48984