Theorem mpteq1d 5181

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

Syntax hints:   → wi 4   = wceq 1541   ↦ cmpt 5172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-opab 5154  df-mpt 5173

This theorem is referenced by:  csbmpt2  5498  mptimass  6022  fmptapd  7105  offval  7619  mposn  8033  offsplitfpar  8049  mpocurryd  8199  cantnff  9564  dfac12lem1  10032  ackbij2lem2  10127  swrd00  14549  swrdlend  14558  swrd0  14563  repswswrd  14688  repswrevw  14691  revco  14738  ccatco  14739  ofccat  14873  vdwapfval  16880  imasdsval  17416  mrcfval  17511  catidd  17583  curfpropd  18136  pwspjmhm  18735  grpinvfval  18888  grpinvfvalALT  18889  psgnfval  19410  psgnfvalfi  19423  odfval  19442  odfvalALT  19443  frgpup3lem  19687  gsum2d2  19884  gsumxp  19886  telgsumfzs  19899  dprd2d2  19956  srgbinom  20147  gsummgp0  20234  pwsco1rhm  20415  pwsco2rhm  20416  funcrngcsetc  20553  funcrngcsetcALT  20554  funcringcsetc  20587  staffval  20754  freshmansdream  21509  phlpropd  21590  pjfval  21641  asclfval  21814  asclpropd  21832  mpfrcl  22018  evlsval  22019  psdffval  22070  evls1rhmlem  22234  evl1fval  22241  mvmulfval  22455  submafval  22492  mdetfval  22499  nfimdetndef  22502  mdetfval1  22503  mdet0pr  22505  m1detdiag  22510  madufval  22550  minmar1fval  22559  gsummatr01  22572  pmatcollpw3fi1lem2  22700  pmatcollpw3fi1  22701  cpmadugsumlemF  22789  ispnrm  23252  ptval2  23514  ptpjcn  23524  xkoptsub  23567  kqval  23639  pt1hmeo  23719  fmval  23856  tmdgsum  24008  subgtgp  24018  prdstmdd  24037  prdsxmslem2  24442  nmfval  24501  lebnumlem1  24885  limcmpt2  25810  dvcmulf  25873  mdegfval  25992  ulmshft  26324  wwlksnextbij  29878  off2  32618  of0r  32655  mptiffisupp  32669  mptprop  32674  fmptunsnop  32676  gsummpt2co  33023  gsumhashmul  33036  gsumwrd2dccat  33042  elrgspnlem4  33207  elrspunidl  33388  evl1deg2  33535  splyval  33577  algextdeglem4  33728  esumnul  34056  ofcfval4  34113  measdivcst  34232  omsfval  34302  signstfval  34572  signstf0  34576  signstfvn  34577  mrsubffval  35539  mrsubfval  35540  msubfval  35556  elmsubrn  35560  mvhfval  35565  msrfval  35569  fwddifval  36195  tailfval  36405  curf  37637  poimirlem24  37683  ftc1anc  37740  sdclem2  37781  erngfset  40837  erngfset-rN  40845  dvhfset  41118  dvhset  41119  zndvdchrrhm  42004  aks4d1p1p6  42105  aks6d1c1  42148  aks6d1c5lem3  42169  sticksstones11  42188  fsuppssindlem2  42624  fsuppssind  42625  mzpclval  42757  mzpcompact2  42784  fsovrfovd  44041  supcnvlimsupmpt  45778  cncfshiftioo  45929  cncfiooicc  45931  dvsinax  45950  iblspltprt  46010  itgspltprt  46016  itgiccshift  46017  dirkercncflem2  46141  fourierdlem90  46233  fourierdlem92  46235  sge0val  46403  sge0prle  46438  sge0ss  46449  sge0iunmptlemfi  46450  sge0p1  46451  sge0iunmptlemre  46452  sge0iunmpt  46455  sge0xp  46466  ismeannd  46504  caratheodorylem1  46563  isomenndlem  46567  hoidmv1lelem2  46629  hoidmvlelem2  46633  hspmbllem2  46664  smflimsuplem1  46857  smflimsuplem4  46860  smflimsuplem7  46863  smflimsup  46865  mgpsumunsn  48391  lmod1zr  48524  iinfssclem1  49085  dfswapf2  49292  swapfval  49293  swapf2vala  49301  swapf2f1o  49307  swapf2f1oaALT  49309  prcofpropd  49410  prcof2a  49420  prcof2  49421  lmdfval  49680  cmdfval  49681