Theorem mpteq1d 5119

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

Syntax hints:   → wi 4   = wceq 1538   ↦ cmpt 5110

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-opab 5093  df-mpt 5111

This theorem is referenced by:  csbmpt2  5410  fmptapd  6910  offval  7396  mposn  7781  offsplitfpar  7798  mpocurryd  7918  cantnff  9121  dfac12lem1  9554  ackbij2lem2  9651  swrd00  13997  swrdlend  14006  swrd0  14011  repswswrd  14137  repswrevw  14140  revco  14187  ccatco  14188  ofccat  14320  vdwapfval  16297  imasdsval  16780  mrcfval  16871  catidd  16943  curfpropd  17475  pwspjmhm  17986  grpinvfval  18134  grpinvfvalALT  18135  psgnfval  18620  psgnfvalfi  18633  odfval  18652  odfvalALT  18653  frgpup3lem  18895  gsum2d2  19087  gsumxp  19089  telgsumfzs  19102  dprd2d2  19159  srgbinom  19288  gsummgp0  19354  pwsco1rhm  19486  pwsco2rhm  19487  staffval  19611  phlpropd  20344  pjfval  20395  asclfval  20565  asclpropd  20583  mpfrcl  20757  evlsval  20758  evls1rhmlem  20945  evl1fval  20952  mvmulfval  21147  submafval  21184  mdetfval  21191  nfimdetndef  21194  mdetfval1  21195  mdet0pr  21197  m1detdiag  21202  madufval  21242  minmar1fval  21251  gsummatr01  21264  pmatcollpw3fi1lem2  21392  pmatcollpw3fi1  21393  cpmadugsumlemF  21481  ispnrm  21944  ptval2  22206  ptpjcn  22216  xkoptsub  22259  kqval  22331  pt1hmeo  22411  fmval  22548  tmdgsum  22700  subgtgp  22710  prdstmdd  22729  prdsxmslem2  23136  nmfval  23195  lebnumlem1  23566  limcmpt2  24487  dvcmulf  24548  mdegfval  24663  ulmshft  24985  wwlksnextbij  27688  off2  30402  mptprop  30458  gsummpt2co  30733  gsumhashmul  30741  freshmansdream  30909  elrspunidl  31014  esumnul  31417  ofcfval4  31474  measdivcst  31593  omsfval  31662  signstfval  31944  signstf0  31948  signstfvn  31949  mrsubffval  32867  mrsubfval  32868  msubfval  32884  elmsubrn  32888  mvhfval  32893  msrfval  32897  fwddifval  33736  tailfval  33833  curf  35035  poimirlem24  35081  ftc1anc  35138  sdclem2  35180  erngfset  38095  erngfset-rN  38103  dvhfset  38376  dvhset  38377  fsuppssindlem2  39458  fsuppssind  39459  mzpclval  39666  mzpcompact2  39693  fsovrfovd  40710  mptima2  41883  supcnvlimsupmpt  42383  cncfshiftioo  42534  cncfiooicc  42536  dvsinax  42555  iblspltprt  42615  itgspltprt  42621  itgiccshift  42622  dirkercncflem2  42746  fourierdlem90  42838  fourierdlem92  42840  sge0val  43005  sge0prle  43040  sge0ss  43051  sge0iunmptlemfi  43052  sge0p1  43053  sge0iunmptlemre  43054  sge0iunmpt  43057  sge0xp  43068  ismeannd  43106  caratheodorylem1  43165  isomenndlem  43169  hoidmv1lelem2  43231  hoidmvlelem2  43235  hspmbllem2  43266  smflimsuplem1  43451  smflimsuplem4  43454  smflimsuplem7  43457  smflimsup  43459  funcrngcsetc  44622  funcrngcsetcALT  44623  funcringcsetc  44659  mgpsumunsn  44763  lmod1zr  44902