Theorem mpteq1d 5202

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

Syntax hints:   → wi 4   = wceq 1570   ↦ cmpt 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5175  df-mpt 5194

This theorem is referenced by:  csbmpt2  5545  mptimass  6077  fmptapd  7171  offval  7685  mposn  8099  offsplitfpar  8115  mpocurryd  8266  cantnff  9644  dfac12lem1  10128  ackbij2lem2  10223  swrd00  14684  swrdlend  14693  swrd0  14698  repswswrd  14823  repswrevw  14826  revco  14873  ccatco  14874  ofccat  15008  vdwapfval  17032  imasdsval  17570  mrcfval  17665  catidd  17737  curfpropd  18290  pwspjmhm  18890  grpinvfval  19046  grpinvfvalALT  19047  psgnfval  19571  psgnfvalfi  19584  odfval  19603  odfvalALT  19604  frgpup3lem  19848  gsum2d2  20045  gsumxp  20047  telgsumfzs  20060  dprd2d2  20117  srgbinom  20314  gsummgp0  20400  pwsco1rhm  20585  pwsco2rhm  20586  funcrngcsetc  20726  funcrngcsetcALT  20727  funcringcsetc  20760  staffval  20925  freshmansdream  21705  phlpropd  21786  pjfval  21837  asclfval  22009  asclpropd  22028  mpfrcl  22217  evlsval  22218  psdffval  22301  evls1rhmlem  22462  evl1fval  22469  mvmulfval  22680  submafval  22717  mdetfval  22724  nfimdetndef  22727  mdetfval1  22728  mdet0pr  22730  m1detdiag  22735  madufval  22775  minmar1fval  22784  gsummatr01  22797  pmatcollpw3fi1lem2  22925  pmatcollpw3fi1  22926  cpmadugsumlemF  23014  ispnrm  23477  ptval2  23739  ptpjcn  23749  xkoptsub  23792  kqval  23864  pt1hmeo  23944  fmval  24081  tmdgsum  24233  subgtgp  24243  prdstmdd  24262  prdsxmslem2  24667  nmfval  24726  lebnumlem1  25101  limcmpt2  26024  dvcmulf  26085  mdegfval  26200  ulmshft  26534  wwlksnextbij  30232  off2  32967  of0r  33005  mptiffisupp  33019  mptprop  33024  fmptunsnop  33026  gsummpt2co  33349  gsumhashmul  33368  gsummulsubdishift1  33369  gsumwrd2dccat  33379  elrgspnlem4  33546  elrspunidl  33717  evl1deg2  33848  ply1coedeg  33860  gsummoncoe1fz  33869  0mplrim  33885  splyval  33930  vietalem  33950  vieta  33951  algextdeglem4  34091  esumnul  34419  ofcfval4  34476  measdivcst  34595  omsfval  34665  signstfval  34932  signstf0  34936  signstfvn  34937  mrsubffval  35980  mrsubfval  35981  msubfval  35997  elmsubrn  36001  mvhfval  36006  msrfval  36010  fwddifval  36635  tailfval  36864  curf  38230  poimirlem24  38276  ftc1anc  38333  sdclem2  38374  erngfset  41554  erngfset-rN  41562  dvhfset  41835  dvhset  41836  zndvdchrrhm  42721  aks4d1p1p6  42821  aks6d1c1  42864  aks6d1c5lem3  42885  sticksstones11  42904  fsuppssindlem2  43307  fsuppssind  43308  mzpclval  43439  mzpcompact2  43466  fsovrfovd  44718  supcnvlimsupmpt  46438  cncfshiftioo  46589  cncfiooicc  46591  dvsinax  46610  iblspltprt  46670  itgspltprt  46676  itgiccshift  46677  dirkercncflem2  46801  fourierdlem90  46893  fourierdlem92  46895  sge0val  47063  sge0prle  47098  sge0ss  47109  sge0iunmptlemfi  47110  sge0p1  47111  sge0iunmptlemre  47112  sge0iunmpt  47115  sge0xp  47126  ismeannd  47164  caratheodorylem1  47223  isomenndlem  47227  hoidmv1lelem2  47289  hoidmvlelem2  47293  hspmbllem2  47324  smflimsuplem1  47517  smflimsuplem4  47520  smflimsuplem7  47523  smflimsup  47525  mgpsumunsn  49124  lmod1zr  49256  iinfssclem1  49815  dfswapf2  50022  swapfval  50023  swapf2vala  50031  swapf2f1o  50037  swapf2f1oaALT  50039  prcofpropd  50140  prcof2a  50150  prcof2  50151  lmdfval  50410  cmdfval  50411