Theorem mpteq2ia 5244

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.)

Hypothesis

Ref	Expression
mpteq2ia.1	⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)

Assertion

Ref	Expression
mpteq2ia	⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Proof of Theorem mpteq2ia

Step	Hyp	Ref	Expression
1		mpteq2ia.1	. . . 4 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)
2	1	adantl 481	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	mpteq2dva 5241	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
4	3	mptru 1546	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   = wceq 1539  ⊤wtru 1540   ∈ wcel 2107   ↦ cmpt 5224

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-opab 5205  df-mpt 5225

This theorem is referenced by:  mpteq2i  5246  partfun  6714  feqresmpt  6977  elfvmptrab  7044  fmptap  7191  offres  8009  resixpfo  8977  dfoi  9552  cantnflem1d  9729  cantnflem1  9730  dfceil2  13880  dfid5  15067  dfid6  15068  cnrecnv  15205  ackbijnn  15865  harmonic  15896  ege2le3  16127  eirrlem  16241  prmrec  16961  imasdsval2  17562  dfinito2  18049  dftermo2  18050  dfinito3  18051  dftermo3  18052  smndex1iidm  18915  smndex2dlinvh  18931  cayleylem1  19431  pmtrprfval  19506  gsumzsplit  19946  gsum2dlem2  19990  dmdprdsplitlem  20058  frlmip  21799  coe1sclmul  22286  coe1sclmul2  22288  mdetunilem9  22627  leordtvallem1  23219  leordtvallem2  23220  txkgen  23661  cnmpt1st  23677  cnmpt2nd  23678  tmdgsum  24104  tsmssplit  24161  cnfldnm  24800  expcn  24897  expcnOLD  24899  pcorev2  25062  pi1xfrcnv  25091  rrxip  25425  mbfi1flim  25759  itg2uba  25779  itg2cnlem1  25797  itg2cnlem2  25798  itgitg2  25843  itgss3  25851  itgless  25853  ibladdlem  25856  itgaddlem1  25859  iblabslem  25864  itggt0  25880  itgcn  25881  limcdif  25912  limcres  25922  cnplimc  25923  dvcobr  25984  dvcobrOLD  25985  dvexp  25992  dveflem  26018  dvef  26019  dvlip  26033  dvlipcn  26034  lhop  26056  tdeglem2  26101  plyid  26249  coeidp  26304  dgrid  26305  pserdvlem2  26473  abelth  26486  dvrelog  26680  logcn  26690  dvlog  26694  advlog  26697  advlogexp  26698  logtayl  26703  logccv  26706  dvcxp1  26783  dvsqrt  26785  dvcncxp1  26786  dvcnsqrt  26787  resqrtcn  26793  loglesqrt  26805  logblog  26836  dvatan  26979  leibpilem2  26985  leibpi  26986  efrlim  27013  efrlimOLD  27014  sqrtlim  27017  amgmlem  27034  emcllem5  27044  lgamgulmlem2  27074  lgam1  27108  chtublem  27256  logfacrlim2  27271  bposlem6  27334  chto1lb  27523  vmadivsum  27527  dchrvmasumlema  27545  mulogsumlem  27576  logdivsum  27578  logsqvma2  27588  log2sumbnd  27589  selberglem1  27590  selberglem3  27592  selberg  27593  selberg2lem  27595  selberg2  27596  pntrmax  27609  pntrsumo1  27610  selbergr  27613  selbergs  27619  pnt2  27658  pnt  27659  ostth2  27682  ostth  27684  hilnormi  31183  bra0  31970  zrhre  34021  qqhre  34022  eulerpartgbij  34375  plymulx  34564  elmrsubrn  35526  faclim  35747  ptrest  37627  poimirlem19  37647  poimirlem20  37648  poimirlem30  37658  ovoliunnfl  37670  voliunnfl  37672  mbfposadd  37675  dvtan  37678  itg2addnclem  37679  ibladdnclem  37684  itgaddnclem1  37686  iblabsnclem  37691  itggt0cn  37698  ftc1anclem4  37704  ftc1anclem5  37705  ftc1anclem6  37706  ftc1anclem7  37707  ftc1anclem8  37708  dvasin  37712  dvacos  37713  areacirclem1  37716  aks6d1c1p5  42114  redvmptabs  42395  readvrec2  42396  readvrec  42397  readvcot  42399  arearect  43232  areaquad  43233  cantnfresb  43342  mptrcllem  43631  dfrcl2  43692  dfrcl3  43693  dftrcl3  43738  dfrtrcl3  43751  dfrtrcl4  43756  lhe4.4ex1a  44353  binomcxplemrat  44374  rnsnf  45194  feqresmptf  45241  limsupresre  45716  limsupvaluzmpt  45737  limsup10ex  45793  liminf10ex  45794  dvnprodlem1  45966  itgsin0pilem1  45970  wallispilem4  46088  wallispi2  46093  stirlinglem1  46094  stirlinglem3  46096  dirkercncflem2  46124  fourierdlem48  46174  fourierdlem49  46175  fourierdlem56  46182  fourierdlem57  46183  fourierdlem58  46184  fourierdlem62  46188  fourierdlem107  46233  fouriersw  46251  etransclem46  46300  sge0tsms  46400  sge0less  46412  sge0iun  46439  meadjun  46482  ovn02  46588  hoidmv1le  46614  hspmbllem2  46647  smflimsuplem3  46842  ackval1  48607  ackval2  48608  ackval3  48609