Theorem mpteq1d 5175

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

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

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5148  df-mpt 5167

This theorem is referenced by:  csbmpt2  5513  mptimass  6038  fmptapd  7126  offval  7640  mposn  8053  offsplitfpar  8069  mpocurryd  8219  cantnff  9595  dfac12lem1  10066  ackbij2lem2  10161  swrd00  14607  swrdlend  14616  swrd0  14621  repswswrd  14746  repswrevw  14749  revco  14796  ccatco  14797  ofccat  14931  vdwapfval  16942  imasdsval  17479  mrcfval  17574  catidd  17646  curfpropd  18199  pwspjmhm  18798  grpinvfval  18954  grpinvfvalALT  18955  psgnfval  19475  psgnfvalfi  19488  odfval  19507  odfvalALT  19508  frgpup3lem  19752  gsum2d2  19949  gsumxp  19951  telgsumfzs  19964  dprd2d2  20021  srgbinom  20212  gsummgp0  20297  pwsco1rhm  20479  pwsco2rhm  20480  funcrngcsetc  20617  funcrngcsetcALT  20618  funcringcsetc  20651  staffval  20818  freshmansdream  21554  phlpropd  21635  pjfval  21686  asclfval  21858  asclpropd  21877  mpfrcl  22063  evlsval  22064  psdffval  22123  evls1rhmlem  22286  evl1fval  22293  mvmulfval  22507  submafval  22544  mdetfval  22551  nfimdetndef  22554  mdetfval1  22555  mdet0pr  22557  m1detdiag  22562  madufval  22602  minmar1fval  22611  gsummatr01  22624  pmatcollpw3fi1lem2  22752  pmatcollpw3fi1  22753  cpmadugsumlemF  22841  ispnrm  23304  ptval2  23566  ptpjcn  23576  xkoptsub  23619  kqval  23691  pt1hmeo  23771  fmval  23908  tmdgsum  24060  subgtgp  24070  prdstmdd  24089  prdsxmslem2  24494  nmfval  24553  lebnumlem1  24928  limcmpt2  25851  dvcmulf  25912  mdegfval  26027  ulmshft  26355  wwlksnextbij  29970  off2  32714  of0r  32752  mptiffisupp  32766  mptprop  32771  fmptunsnop  32773  gsummpt2co  33109  gsumhashmul  33128  gsummulsubdishift1  33129  gsumwrd2dccat  33139  elrgspnlem4  33306  elrspunidl  33488  evl1deg2  33637  ply1coedeg  33649  gsummoncoe1fz  33658  splyval  33703  vietalem  33723  vieta  33724  algextdeglem4  33864  esumnul  34192  ofcfval4  34249  measdivcst  34368  omsfval  34438  signstfval  34708  signstf0  34712  signstfvn  34713  mrsubffval  35689  mrsubfval  35690  msubfval  35706  elmsubrn  35710  mvhfval  35715  msrfval  35719  fwddifval  36344  tailfval  36554  curf  37919  poimirlem24  37965  ftc1anc  38022  sdclem2  38063  erngfset  41245  erngfset-rN  41253  dvhfset  41526  dvhset  41527  zndvdchrrhm  42412  aks4d1p1p6  42512  aks6d1c1  42555  aks6d1c5lem3  42576  sticksstones11  42595  fsuppssindlem2  43025  fsuppssind  43026  mzpclval  43157  mzpcompact2  43184  fsovrfovd  44436  supcnvlimsupmpt  46169  cncfshiftioo  46320  cncfiooicc  46322  dvsinax  46341  iblspltprt  46401  itgspltprt  46407  itgiccshift  46408  dirkercncflem2  46532  fourierdlem90  46624  fourierdlem92  46626  sge0val  46794  sge0prle  46829  sge0ss  46840  sge0iunmptlemfi  46841  sge0p1  46842  sge0iunmptlemre  46843  sge0iunmpt  46846  sge0xp  46857  ismeannd  46895  caratheodorylem1  46954  isomenndlem  46958  hoidmv1lelem2  47020  hoidmvlelem2  47024  hspmbllem2  47055  smflimsuplem1  47248  smflimsuplem4  47251  smflimsuplem7  47254  smflimsup  47256  mgpsumunsn  48837  lmod1zr  48969  iinfssclem1  49529  dfswapf2  49736  swapfval  49737  swapf2vala  49745  swapf2f1o  49751  swapf2f1oaALT  49753  prcofpropd  49854  prcof2a  49864  prcof2  49865  lmdfval  50124  cmdfval  50125