Theorem mpteq1d 5261

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

Syntax hints:   → wi 4   = wceq 1537   ↦ cmpt 5249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-opab 5229  df-mpt 5250

This theorem is referenced by:  csbmpt2  5577  mptimass  6102  fmptapd  7205  offval  7723  mposn  8144  offsplitfpar  8160  mpocurryd  8310  cantnff  9743  dfac12lem1  10213  ackbij2lem2  10308  swrd00  14692  swrdlend  14701  swrd0  14706  repswswrd  14832  repswrevw  14835  revco  14883  ccatco  14884  ofccat  15018  vdwapfval  17018  imasdsval  17575  mrcfval  17666  catidd  17738  curfpropd  18303  pwspjmhm  18865  grpinvfval  19018  grpinvfvalALT  19019  psgnfval  19542  psgnfvalfi  19555  odfval  19574  odfvalALT  19575  frgpup3lem  19819  gsum2d2  20016  gsumxp  20018  telgsumfzs  20031  dprd2d2  20088  srgbinom  20258  gsummgp0  20341  pwsco1rhm  20528  pwsco2rhm  20529  funcrngcsetc  20662  funcrngcsetcALT  20663  funcringcsetc  20696  staffval  20864  freshmansdream  21616  phlpropd  21696  pjfval  21749  asclfval  21922  asclpropd  21940  mpfrcl  22132  evlsval  22133  psdffval  22184  evls1rhmlem  22346  evl1fval  22353  mvmulfval  22569  submafval  22606  mdetfval  22613  nfimdetndef  22616  mdetfval1  22617  mdet0pr  22619  m1detdiag  22624  madufval  22664  minmar1fval  22673  gsummatr01  22686  pmatcollpw3fi1lem2  22814  pmatcollpw3fi1  22815  cpmadugsumlemF  22903  ispnrm  23368  ptval2  23630  ptpjcn  23640  xkoptsub  23683  kqval  23755  pt1hmeo  23835  fmval  23972  tmdgsum  24124  subgtgp  24134  prdstmdd  24153  prdsxmslem2  24563  nmfval  24622  lebnumlem1  25012  limcmpt2  25939  dvcmulf  26002  mdegfval  26121  ulmshft  26451  wwlksnextbij  29935  off2  32660  of0r  32696  mptiffisupp  32705  mptprop  32710  gsummpt2co  33031  gsumhashmul  33040  elrspunidl  33421  evl1deg2  33567  algextdeglem4  33711  esumnul  34012  ofcfval4  34069  measdivcst  34188  omsfval  34259  signstfval  34541  signstf0  34545  signstfvn  34546  mrsubffval  35475  mrsubfval  35476  msubfval  35492  elmsubrn  35496  mvhfval  35501  msrfval  35505  fwddifval  36126  tailfval  36338  curf  37558  poimirlem24  37604  ftc1anc  37661  sdclem2  37702  erngfset  40756  erngfset-rN  40764  dvhfset  41037  dvhset  41038  zndvdchrrhm  41927  aks4d1p1p6  42030  aks6d1c1  42073  aks6d1c5lem3  42094  sticksstones11  42113  fsuppssindlem2  42547  fsuppssind  42548  mzpclval  42681  mzpcompact2  42708  fsovrfovd  43971  supcnvlimsupmpt  45662  cncfshiftioo  45813  cncfiooicc  45815  dvsinax  45834  iblspltprt  45894  itgspltprt  45900  itgiccshift  45901  dirkercncflem2  46025  fourierdlem90  46117  fourierdlem92  46119  sge0val  46287  sge0prle  46322  sge0ss  46333  sge0iunmptlemfi  46334  sge0p1  46335  sge0iunmptlemre  46336  sge0iunmpt  46339  sge0xp  46350  ismeannd  46388  caratheodorylem1  46447  isomenndlem  46451  hoidmv1lelem2  46513  hoidmvlelem2  46517  hspmbllem2  46548  smflimsuplem1  46741  smflimsuplem4  46744  smflimsuplem7  46747  smflimsup  46749  mgpsumunsn  48086  lmod1zr  48222