Theorem mpteq1d 5183

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

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

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-opab 5156  df-mpt 5175

This theorem is referenced by:  csbmpt2  5501  mptimass  6026  fmptapd  7111  offval  7625  mposn  8039  offsplitfpar  8055  mpocurryd  8205  cantnff  9571  dfac12lem1  10042  ackbij2lem2  10137  swrd00  14554  swrdlend  14563  swrd0  14568  repswswrd  14693  repswrevw  14696  revco  14743  ccatco  14744  ofccat  14878  vdwapfval  16885  imasdsval  17421  mrcfval  17516  catidd  17588  curfpropd  18141  pwspjmhm  18740  grpinvfval  18893  grpinvfvalALT  18894  psgnfval  19414  psgnfvalfi  19427  odfval  19446  odfvalALT  19447  frgpup3lem  19691  gsum2d2  19888  gsumxp  19890  telgsumfzs  19903  dprd2d2  19960  srgbinom  20151  gsummgp0  20238  pwsco1rhm  20419  pwsco2rhm  20420  funcrngcsetc  20557  funcrngcsetcALT  20558  funcringcsetc  20591  staffval  20758  freshmansdream  21513  phlpropd  21594  pjfval  21645  asclfval  21818  asclpropd  21836  mpfrcl  22021  evlsval  22022  psdffval  22073  evls1rhmlem  22237  evl1fval  22244  mvmulfval  22458  submafval  22495  mdetfval  22502  nfimdetndef  22505  mdetfval1  22506  mdet0pr  22508  m1detdiag  22513  madufval  22553  minmar1fval  22562  gsummatr01  22575  pmatcollpw3fi1lem2  22703  pmatcollpw3fi1  22704  cpmadugsumlemF  22792  ispnrm  23255  ptval2  23517  ptpjcn  23527  xkoptsub  23570  kqval  23642  pt1hmeo  23722  fmval  23859  tmdgsum  24011  subgtgp  24021  prdstmdd  24040  prdsxmslem2  24445  nmfval  24504  lebnumlem1  24888  limcmpt2  25813  dvcmulf  25876  mdegfval  25995  ulmshft  26327  wwlksnextbij  29882  off2  32625  of0r  32664  mptiffisupp  32678  mptprop  32683  fmptunsnop  32685  gsummpt2co  33035  gsumhashmul  33048  gsumwrd2dccat  33054  elrgspnlem4  33219  elrspunidl  33400  evl1deg2  33547  splyval  33600  algextdeglem4  33754  esumnul  34082  ofcfval4  34139  measdivcst  34258  omsfval  34328  signstfval  34598  signstf0  34602  signstfvn  34603  mrsubffval  35572  mrsubfval  35573  msubfval  35589  elmsubrn  35593  mvhfval  35598  msrfval  35602  fwddifval  36227  tailfval  36437  curf  37659  poimirlem24  37705  ftc1anc  37762  sdclem2  37803  erngfset  40919  erngfset-rN  40927  dvhfset  41200  dvhset  41201  zndvdchrrhm  42086  aks4d1p1p6  42187  aks6d1c1  42230  aks6d1c5lem3  42251  sticksstones11  42270  fsuppssindlem2  42711  fsuppssind  42712  mzpclval  42843  mzpcompact2  42870  fsovrfovd  44127  supcnvlimsupmpt  45864  cncfshiftioo  46015  cncfiooicc  46017  dvsinax  46036  iblspltprt  46096  itgspltprt  46102  itgiccshift  46103  dirkercncflem2  46227  fourierdlem90  46319  fourierdlem92  46321  sge0val  46489  sge0prle  46524  sge0ss  46535  sge0iunmptlemfi  46536  sge0p1  46537  sge0iunmptlemre  46538  sge0iunmpt  46541  sge0xp  46552  ismeannd  46590  caratheodorylem1  46649  isomenndlem  46653  hoidmv1lelem2  46715  hoidmvlelem2  46719  hspmbllem2  46750  smflimsuplem1  46943  smflimsuplem4  46946  smflimsuplem7  46949  smflimsup  46951  mgpsumunsn  48486  lmod1zr  48619  iinfssclem1  49180  dfswapf2  49387  swapfval  49388  swapf2vala  49396  swapf2f1o  49402  swapf2f1oaALT  49404  prcofpropd  49505  prcof2a  49515  prcof2  49516  lmdfval  49775  cmdfval  49776