Theorem mpteq1d 5165

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

Syntax hints:   → wi 4   = wceq 1539   ↦ cmpt 5153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-opab 5133  df-mpt 5154

This theorem is referenced by:  csbmpt2  5464  fmptapd  7025  offval  7520  mposn  7914  offsplitfpar  7931  mpocurryd  8056  cantnff  9362  dfac12lem1  9830  ackbij2lem2  9927  swrd00  14285  swrdlend  14294  swrd0  14299  repswswrd  14425  repswrevw  14428  revco  14475  ccatco  14476  ofccat  14608  vdwapfval  16600  imasdsval  17143  mrcfval  17234  catidd  17306  curfpropd  17867  pwspjmhm  18383  grpinvfval  18533  grpinvfvalALT  18534  psgnfval  19023  psgnfvalfi  19036  odfval  19055  odfvalALT  19056  frgpup3lem  19298  gsum2d2  19490  gsumxp  19492  telgsumfzs  19505  dprd2d2  19562  srgbinom  19696  gsummgp0  19762  pwsco1rhm  19897  pwsco2rhm  19898  staffval  20022  phlpropd  20772  pjfval  20823  asclfval  20993  asclpropd  21011  mpfrcl  21205  evlsval  21206  evls1rhmlem  21397  evl1fval  21404  mvmulfval  21599  submafval  21636  mdetfval  21643  nfimdetndef  21646  mdetfval1  21647  mdet0pr  21649  m1detdiag  21654  madufval  21694  minmar1fval  21703  gsummatr01  21716  pmatcollpw3fi1lem2  21844  pmatcollpw3fi1  21845  cpmadugsumlemF  21933  ispnrm  22398  ptval2  22660  ptpjcn  22670  xkoptsub  22713  kqval  22785  pt1hmeo  22865  fmval  23002  tmdgsum  23154  subgtgp  23164  prdstmdd  23183  prdsxmslem2  23591  nmfval  23650  lebnumlem1  24030  limcmpt2  24953  dvcmulf  25014  mdegfval  25132  ulmshft  25454  wwlksnextbij  28168  off2  30879  mptprop  30933  gsummpt2co  31210  gsumhashmul  31218  freshmansdream  31386  elrspunidl  31508  esumnul  31916  ofcfval4  31973  measdivcst  32092  omsfval  32161  signstfval  32443  signstf0  32447  signstfvn  32448  mrsubffval  33369  mrsubfval  33370  msubfval  33386  elmsubrn  33390  mvhfval  33395  msrfval  33399  fwddifval  34391  tailfval  34488  curf  35682  poimirlem24  35728  ftc1anc  35785  sdclem2  35827  erngfset  38740  erngfset-rN  38748  dvhfset  39021  dvhset  39022  aks4d1p1p6  40009  sticksstones11  40040  fsuppssindlem2  40204  fsuppssind  40205  mzpclval  40463  mzpcompact2  40490  fsovrfovd  41506  mptima2  42680  supcnvlimsupmpt  43172  cncfshiftioo  43323  cncfiooicc  43325  dvsinax  43344  iblspltprt  43404  itgspltprt  43410  itgiccshift  43411  dirkercncflem2  43535  fourierdlem90  43627  fourierdlem92  43629  sge0val  43794  sge0prle  43829  sge0ss  43840  sge0iunmptlemfi  43841  sge0p1  43842  sge0iunmptlemre  43843  sge0iunmpt  43846  sge0xp  43857  ismeannd  43895  caratheodorylem1  43954  isomenndlem  43958  hoidmv1lelem2  44020  hoidmvlelem2  44024  hspmbllem2  44055  smflimsuplem1  44240  smflimsuplem4  44243  smflimsuplem7  44246  smflimsup  44248  funcrngcsetc  45444  funcrngcsetcALT  45445  funcringcsetc  45481  mgpsumunsn  45585  lmod1zr  45722