Theorem mpteq1d 4666

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

Syntax hints:   → wi 4   = wceq 1475   ↦ cmpt 4643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ral 2901  df-opab 4644  df-mpt 4645

This theorem is referenced by:  csbmpt2  4935  fmptapd  6342  offval  6802  mpt2sn  7155  mpt2curryd  7282  cantnff  8454  dfac12lem1  8848  ackbij2lem2  8945  swrd00  13270  swrd0val  13273  swrdlend  13283  swrd0  13286  repswswrd  13382  repswrevw  13384  revco  13431  ccatco  13432  ofccat  13556  vdwapfval  15513  imasdsval  15998  mrcfval  16091  catidd  16164  curfpropd  16696  pwspjmhm  17191  grpinvfval  17283  psgnfval  17743  psgnfvalfi  17756  odfval  17775  frgpup3lem  18013  gsum2d2  18196  gsumxp  18198  telgsumfzs  18209  dprd2d2  18266  srgbinom  18368  gsummgp0  18431  pwsco1rhm  18561  pwsco2rhm  18562  staffval  18670  asclfval  19155  asclpropd  19167  mpfrcl  19339  evlsval  19340  evls1rhmlem  19507  evl1fval  19513  phlpropd  19819  pjfval  19869  mvmulfval  20167  submafval  20204  mdetfval  20211  nfimdetndef  20214  mdetfval1  20215  mdet0pr  20217  m1detdiag  20222  madufval  20262  minmar1fval  20271  gsummatr01  20284  pmatcollpw3fi1lem2  20411  pmatcollpw3fi1  20412  cpmadugsumlemF  20500  ispnrm  20953  ptval2  21214  ptpjcn  21224  xkoptsub  21267  kqval  21339  pt1hmeo  21419  fmval  21557  tmdgsum  21709  subgtgp  21719  prdstmdd  21737  prdsxmslem2  22144  nmfval  22203  lebnumlem1  22568  limcmpt2  23454  dvcmulf  23514  mdegfval  23626  ulmshft  23948  wwlkextbij  26261  off2  28823  gsummpt2co  29111  esumnul  29437  ofcfval4  29494  measdivcst  29615  omsfval  29683  signstfval  29967  signstf0  29971  signstfvn  29972  mrsubffval  30658  mrsubfval  30659  msubfval  30675  elmsubrn  30679  mvhfval  30684  msrfval  30688  fwddifval  31439  tailfval  31537  curf  32557  poimirlem24  32603  ftc1anc  32663  sdclem2  32708  erngfset  35105  erngfset-rN  35113  dvhfset  35387  dvhset  35388  mzpclval  36306  mzpcompact2  36333  fsovrfovd  37323  cncfshiftioo  38778  cncfiooicc  38780  dvsinax  38801  iblspltprt  38865  itgspltprt  38871  itgiccshift  38872  dirkercncflem2  38997  fourierdlem90  39089  fourierdlem92  39091  sge0val  39259  sge0prle  39294  sge0ss  39305  sge0iunmptlemfi  39306  sge0p1  39307  sge0iunmptlemre  39308  sge0iunmpt  39311  sge0xp  39322  ismeannd  39360  caratheodorylem1  39416  isomenndlem  39420  hoidmv1lelem2  39482  hoidmvlelem2  39486  hspmbllem2  39517  wwlksnextbij  41108  funcrngcsetc  41790  funcrngcsetcALT  41791  funcringcsetc  41827  mgpsumunsn  41933  lmod1zr  42076