Theorem mpteq1d 5120

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-12 2178  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-opab 5094  df-mpt 5112

This theorem is referenced by:  csbmpt2  5414  fmptapd  6944  offval  7434  mposn  7825  offsplitfpar  7842  mpocurryd  7965  cantnff  9211  dfac12lem1  9644  ackbij2lem2  9741  swrd00  14096  swrdlend  14105  swrd0  14110  repswswrd  14236  repswrevw  14239  revco  14286  ccatco  14287  ofccat  14419  vdwapfval  16408  imasdsval  16892  mrcfval  16983  catidd  17055  curfpropd  17600  pwspjmhm  18111  grpinvfval  18261  grpinvfvalALT  18262  psgnfval  18747  psgnfvalfi  18760  odfval  18779  odfvalALT  18780  frgpup3lem  19022  gsum2d2  19214  gsumxp  19216  telgsumfzs  19229  dprd2d2  19286  srgbinom  19415  gsummgp0  19481  pwsco1rhm  19613  pwsco2rhm  19614  staffval  19738  phlpropd  20472  pjfval  20523  asclfval  20693  asclpropd  20712  mpfrcl  20900  evlsval  20901  evls1rhmlem  21092  evl1fval  21099  mvmulfval  21294  submafval  21331  mdetfval  21338  nfimdetndef  21341  mdetfval1  21342  mdet0pr  21344  m1detdiag  21349  madufval  21389  minmar1fval  21398  gsummatr01  21411  pmatcollpw3fi1lem2  21539  pmatcollpw3fi1  21540  cpmadugsumlemF  21628  ispnrm  22091  ptval2  22353  ptpjcn  22363  xkoptsub  22406  kqval  22478  pt1hmeo  22558  fmval  22695  tmdgsum  22847  subgtgp  22857  prdstmdd  22876  prdsxmslem2  23283  nmfval  23342  lebnumlem1  23714  limcmpt2  24636  dvcmulf  24697  mdegfval  24815  ulmshft  25137  wwlksnextbij  27840  off2  30552  mptprop  30606  gsummpt2co  30885  gsumhashmul  30893  freshmansdream  31061  elrspunidl  31178  esumnul  31586  ofcfval4  31643  measdivcst  31762  omsfval  31831  signstfval  32113  signstf0  32117  signstfvn  32118  mrsubffval  33040  mrsubfval  33041  msubfval  33057  elmsubrn  33061  mvhfval  33066  msrfval  33070  fwddifval  34102  tailfval  34199  curf  35375  poimirlem24  35421  ftc1anc  35478  sdclem2  35520  erngfset  38433  erngfset-rN  38441  dvhfset  38714  dvhset  38715  aks4d1p1p6  39697  fsuppssindlem2  39852  fsuppssind  39853  mzpclval  40111  mzpcompact2  40138  fsovrfovd  41155  mptima2  42320  supcnvlimsupmpt  42816  cncfshiftioo  42967  cncfiooicc  42969  dvsinax  42988  iblspltprt  43048  itgspltprt  43054  itgiccshift  43055  dirkercncflem2  43179  fourierdlem90  43271  fourierdlem92  43273  sge0val  43438  sge0prle  43473  sge0ss  43484  sge0iunmptlemfi  43485  sge0p1  43486  sge0iunmptlemre  43487  sge0iunmpt  43490  sge0xp  43501  ismeannd  43539  caratheodorylem1  43598  isomenndlem  43602  hoidmv1lelem2  43664  hoidmvlelem2  43668  hspmbllem2  43699  smflimsuplem1  43884  smflimsuplem4  43887  smflimsuplem7  43890  smflimsup  43892  funcrngcsetc  45082  funcrngcsetcALT  45083  funcringcsetc  45119  mgpsumunsn  45223  lmod1zr  45360