Theorem mpteq1d 5190

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5163  df-mpt 5182

This theorem is referenced by:  csbmpt2  5514  mptimass  6040  fmptapd  7127  offval  7641  mposn  8055  offsplitfpar  8071  mpocurryd  8221  cantnff  9595  dfac12lem1  10066  ackbij2lem2  10161  swrd00  14580  swrdlend  14589  swrd0  14594  repswswrd  14719  repswrevw  14722  revco  14769  ccatco  14770  ofccat  14904  vdwapfval  16911  imasdsval  17448  mrcfval  17543  catidd  17615  curfpropd  18168  pwspjmhm  18767  grpinvfval  18920  grpinvfvalALT  18921  psgnfval  19441  psgnfvalfi  19454  odfval  19473  odfvalALT  19474  frgpup3lem  19718  gsum2d2  19915  gsumxp  19917  telgsumfzs  19930  dprd2d2  19987  srgbinom  20178  gsummgp0  20265  pwsco1rhm  20447  pwsco2rhm  20448  funcrngcsetc  20585  funcrngcsetcALT  20586  funcringcsetc  20619  staffval  20786  freshmansdream  21541  phlpropd  21622  pjfval  21673  asclfval  21846  asclpropd  21865  mpfrcl  22052  evlsval  22053  psdffval  22112  evls1rhmlem  22277  evl1fval  22284  mvmulfval  22498  submafval  22535  mdetfval  22542  nfimdetndef  22545  mdetfval1  22546  mdet0pr  22548  m1detdiag  22553  madufval  22593  minmar1fval  22602  gsummatr01  22615  pmatcollpw3fi1lem2  22743  pmatcollpw3fi1  22744  cpmadugsumlemF  22832  ispnrm  23295  ptval2  23557  ptpjcn  23567  xkoptsub  23610  kqval  23682  pt1hmeo  23762  fmval  23899  tmdgsum  24051  subgtgp  24061  prdstmdd  24080  prdsxmslem2  24485  nmfval  24544  lebnumlem1  24928  limcmpt2  25853  dvcmulf  25916  mdegfval  26035  ulmshft  26367  wwlksnextbij  29987  off2  32730  of0r  32768  mptiffisupp  32782  mptprop  32787  fmptunsnop  32789  gsummpt2co  33141  gsumhashmul  33160  gsummulsubdishift1  33161  gsumwrd2dccat  33171  elrgspnlem4  33338  elrspunidl  33520  evl1deg2  33669  ply1coedeg  33681  gsummoncoe1fz  33690  splyval  33735  vietalem  33755  vieta  33756  algextdeglem4  33897  esumnul  34225  ofcfval4  34282  measdivcst  34401  omsfval  34471  signstfval  34741  signstf0  34745  signstfvn  34746  mrsubffval  35720  mrsubfval  35721  msubfval  35737  elmsubrn  35741  mvhfval  35746  msrfval  35750  fwddifval  36375  tailfval  36585  curf  37843  poimirlem24  37889  ftc1anc  37946  sdclem2  37987  erngfset  41169  erngfset-rN  41177  dvhfset  41450  dvhset  41451  zndvdchrrhm  42336  aks4d1p1p6  42437  aks6d1c1  42480  aks6d1c5lem3  42501  sticksstones11  42520  fsuppssindlem2  42944  fsuppssind  42945  mzpclval  43076  mzpcompact2  43103  fsovrfovd  44359  supcnvlimsupmpt  46093  cncfshiftioo  46244  cncfiooicc  46246  dvsinax  46265  iblspltprt  46325  itgspltprt  46331  itgiccshift  46332  dirkercncflem2  46456  fourierdlem90  46548  fourierdlem92  46550  sge0val  46718  sge0prle  46753  sge0ss  46764  sge0iunmptlemfi  46765  sge0p1  46766  sge0iunmptlemre  46767  sge0iunmpt  46770  sge0xp  46781  ismeannd  46819  caratheodorylem1  46878  isomenndlem  46882  hoidmv1lelem2  46944  hoidmvlelem2  46948  hspmbllem2  46979  smflimsuplem1  47172  smflimsuplem4  47175  smflimsuplem7  47178  smflimsup  47180  mgpsumunsn  48715  lmod1zr  48847  iinfssclem1  49407  dfswapf2  49614  swapfval  49615  swapf2vala  49623  swapf2f1o  49629  swapf2f1oaALT  49631  prcofpropd  49732  prcof2a  49742  prcof2  49743  lmdfval  50002  cmdfval  50003