Theorem mpteq1d 5197

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5170  df-mpt 5189

This theorem is referenced by:  csbmpt2  5518  mptimass  6044  fmptapd  7145  offval  7662  mposn  8082  offsplitfpar  8098  mpocurryd  8248  cantnff  9627  dfac12lem1  10097  ackbij2lem2  10192  swrd00  14609  swrdlend  14618  swrd0  14623  repswswrd  14749  repswrevw  14752  revco  14800  ccatco  14801  ofccat  14935  vdwapfval  16942  imasdsval  17478  mrcfval  17569  catidd  17641  curfpropd  18194  pwspjmhm  18757  grpinvfval  18910  grpinvfvalALT  18911  psgnfval  19430  psgnfvalfi  19443  odfval  19462  odfvalALT  19463  frgpup3lem  19707  gsum2d2  19904  gsumxp  19906  telgsumfzs  19919  dprd2d2  19976  srgbinom  20140  gsummgp0  20227  pwsco1rhm  20411  pwsco2rhm  20412  funcrngcsetc  20549  funcrngcsetcALT  20550  funcringcsetc  20583  staffval  20750  freshmansdream  21484  phlpropd  21564  pjfval  21615  asclfval  21788  asclpropd  21806  mpfrcl  21992  evlsval  21993  psdffval  22044  evls1rhmlem  22208  evl1fval  22215  mvmulfval  22429  submafval  22466  mdetfval  22473  nfimdetndef  22476  mdetfval1  22477  mdet0pr  22479  m1detdiag  22484  madufval  22524  minmar1fval  22533  gsummatr01  22546  pmatcollpw3fi1lem2  22674  pmatcollpw3fi1  22675  cpmadugsumlemF  22763  ispnrm  23226  ptval2  23488  ptpjcn  23498  xkoptsub  23541  kqval  23613  pt1hmeo  23693  fmval  23830  tmdgsum  23982  subgtgp  23992  prdstmdd  24011  prdsxmslem2  24417  nmfval  24476  lebnumlem1  24860  limcmpt2  25785  dvcmulf  25848  mdegfval  25967  ulmshft  26299  wwlksnextbij  29832  off2  32565  of0r  32602  mptiffisupp  32616  mptprop  32621  fmptunsnop  32623  gsummpt2co  32988  gsumhashmul  33001  gsumwrd2dccat  33007  elrgspnlem4  33196  elrspunidl  33399  evl1deg2  33546  algextdeglem4  33710  esumnul  34038  ofcfval4  34095  measdivcst  34214  omsfval  34285  signstfval  34555  signstf0  34559  signstfvn  34560  mrsubffval  35494  mrsubfval  35495  msubfval  35511  elmsubrn  35515  mvhfval  35520  msrfval  35524  fwddifval  36150  tailfval  36360  curf  37592  poimirlem24  37638  ftc1anc  37695  sdclem2  37736  erngfset  40793  erngfset-rN  40801  dvhfset  41074  dvhset  41075  zndvdchrrhm  41960  aks4d1p1p6  42061  aks6d1c1  42104  aks6d1c5lem3  42125  sticksstones11  42144  fsuppssindlem2  42580  fsuppssind  42581  mzpclval  42713  mzpcompact2  42740  fsovrfovd  43998  supcnvlimsupmpt  45739  cncfshiftioo  45890  cncfiooicc  45892  dvsinax  45911  iblspltprt  45971  itgspltprt  45977  itgiccshift  45978  dirkercncflem2  46102  fourierdlem90  46194  fourierdlem92  46196  sge0val  46364  sge0prle  46399  sge0ss  46410  sge0iunmptlemfi  46411  sge0p1  46412  sge0iunmptlemre  46413  sge0iunmpt  46416  sge0xp  46427  ismeannd  46465  caratheodorylem1  46524  isomenndlem  46528  hoidmv1lelem2  46590  hoidmvlelem2  46594  hspmbllem2  46625  smflimsuplem1  46818  smflimsuplem4  46821  smflimsuplem7  46824  smflimsup  46826  mgpsumunsn  48349  lmod1zr  48482  iinfssclem1  49043  dfswapf2  49250  swapfval  49251  swapf2vala  49259  swapf2f1o  49265  swapf2f1oaALT  49267  prcofpropd  49368  prcof2a  49378  prcof2  49379  lmdfval  49638  cmdfval  49639