Theorem mpteq1d 5148

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

Syntax hints:   → wi 4   = wceq 1533   ↦ cmpt 5139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-opab 5122  df-mpt 5140

This theorem is referenced by:  csbmpt2  5438  fmptapd  6928  offval  7410  mposn  7792  offsplitfpar  7809  mpocurryd  7929  cantnff  9131  dfac12lem1  9563  ackbij2lem2  9656  swrd00  14000  swrdlend  14009  swrd0  14014  repswswrd  14140  repswrevw  14143  revco  14190  ccatco  14191  ofccat  14323  vdwapfval  16301  imasdsval  16782  mrcfval  16873  catidd  16945  curfpropd  17477  pwspjmhm  17988  grpinvfval  18136  grpinvfvalALT  18137  psgnfval  18622  psgnfvalfi  18635  odfval  18654  odfvalALT  18655  frgpup3lem  18897  gsum2d2  19088  gsumxp  19090  telgsumfzs  19103  dprd2d2  19160  srgbinom  19289  gsummgp0  19352  pwsco1rhm  19484  pwsco2rhm  19485  staffval  19612  asclfval  20102  asclpropd  20120  mpfrcl  20292  evlsval  20293  evls1rhmlem  20478  evl1fval  20485  phlpropd  20793  pjfval  20844  mvmulfval  21145  submafval  21182  mdetfval  21189  nfimdetndef  21192  mdetfval1  21193  mdet0pr  21195  m1detdiag  21200  madufval  21240  minmar1fval  21249  gsummatr01  21262  pmatcollpw3fi1lem2  21389  pmatcollpw3fi1  21390  cpmadugsumlemF  21478  ispnrm  21941  ptval2  22203  ptpjcn  22213  xkoptsub  22256  kqval  22328  pt1hmeo  22408  fmval  22545  tmdgsum  22697  subgtgp  22707  prdstmdd  22726  prdsxmslem2  23133  nmfval  23192  lebnumlem1  23559  limcmpt2  24476  dvcmulf  24536  mdegfval  24650  ulmshft  24972  wwlksnextbij  27674  off2  30382  mptprop  30428  gsummpt2co  30681  freshmansdream  30854  esumnul  31302  ofcfval4  31359  measdivcst  31478  omsfval  31547  signstfval  31829  signstf0  31833  signstfvn  31834  mrsubffval  32749  mrsubfval  32750  msubfval  32766  elmsubrn  32770  mvhfval  32775  msrfval  32779  fwddifval  33618  tailfval  33715  curf  34864  poimirlem24  34910  ftc1anc  34969  sdclem2  35011  erngfset  37929  erngfset-rN  37937  dvhfset  38210  dvhset  38211  mzpclval  39315  mzpcompact2  39342  fsovrfovd  40348  mptima2  41509  supcnvlimsupmpt  42014  cncfshiftioo  42167  cncfiooicc  42169  dvsinax  42189  iblspltprt  42250  itgspltprt  42256  itgiccshift  42257  dirkercncflem2  42382  fourierdlem90  42474  fourierdlem92  42476  sge0val  42641  sge0prle  42676  sge0ss  42687  sge0iunmptlemfi  42688  sge0p1  42689  sge0iunmptlemre  42690  sge0iunmpt  42693  sge0xp  42704  ismeannd  42742  caratheodorylem1  42801  isomenndlem  42805  hoidmv1lelem2  42867  hoidmvlelem2  42871  hspmbllem2  42902  smflimsuplem1  43087  smflimsuplem4  43090  smflimsuplem7  43093  smflimsup  43095  funcrngcsetc  44262  funcrngcsetcALT  44263  funcringcsetc  44299  mgpsumunsn  44402  lmod1zr  44541