Theorem mpteq2ia 5269

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 5266	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
4	3	mptru 1544	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   = wceq 1537  ⊤wtru 1538   ∈ wcel 2108   ↦ cmpt 5249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-opab 5229  df-mpt 5250

This theorem is referenced by:  mpteq2i  5271  partfun  6727  feqresmpt  6991  elfvmptrab  7058  fmptap  7204  offres  8024  resixpfo  8994  dfoi  9580  cantnflem1d  9757  cantnflem1  9758  dfceil2  13890  dfid5  15076  dfid6  15077  cnrecnv  15214  ackbijnn  15876  harmonic  15907  ege2le3  16138  eirrlem  16252  prmrec  16969  imasdsval2  17576  dfinito2  18070  dftermo2  18071  dfinito3  18072  dftermo3  18073  smndex1iidm  18936  smndex2dlinvh  18952  cayleylem1  19454  pmtrprfval  19529  gsumzsplit  19969  gsum2dlem2  20013  dmdprdsplitlem  20081  frlmip  21821  coe1sclmul  22306  coe1sclmul2  22308  mdetunilem9  22647  leordtvallem1  23239  leordtvallem2  23240  txkgen  23681  cnmpt1st  23697  cnmpt2nd  23698  tmdgsum  24124  tsmssplit  24181  cnfldnm  24820  expcn  24915  expcnOLD  24917  pcorev2  25080  pi1xfrcnv  25109  rrxip  25443  mbfi1flim  25778  itg2uba  25798  itg2cnlem1  25816  itg2cnlem2  25817  itgitg2  25862  itgss3  25870  itgless  25872  ibladdlem  25875  itgaddlem1  25878  iblabslem  25883  itggt0  25899  itgcn  25900  limcdif  25931  limcres  25941  cnplimc  25942  dvcobr  26003  dvcobrOLD  26004  dvexp  26011  dveflem  26037  dvef  26038  dvlip  26052  dvlipcn  26053  lhop  26075  tdeglem2  26120  plyid  26268  coeidp  26323  dgrid  26324  pserdvlem2  26490  abelth  26503  dvrelog  26697  logcn  26707  dvlog  26711  advlog  26714  advlogexp  26715  logtayl  26720  logccv  26723  dvcxp1  26800  dvsqrt  26802  dvcncxp1  26803  dvcnsqrt  26804  resqrtcn  26810  loglesqrt  26822  logblog  26853  dvatan  26996  leibpilem2  27002  leibpi  27003  efrlim  27030  efrlimOLD  27031  sqrtlim  27034  amgmlem  27051  emcllem5  27061  lgamgulmlem2  27091  lgam1  27125  chtublem  27273  logfacrlim2  27288  bposlem6  27351  chto1lb  27540  vmadivsum  27544  dchrvmasumlema  27562  mulogsumlem  27593  logdivsum  27595  logsqvma2  27605  log2sumbnd  27606  selberglem1  27607  selberglem3  27609  selberg  27610  selberg2lem  27612  selberg2  27613  pntrmax  27626  pntrsumo1  27627  selbergr  27630  selbergs  27636  pnt2  27675  pnt  27676  ostth2  27699  ostth  27701  hilnormi  31195  bra0  31982  zrhre  33965  qqhre  33966  eulerpartgbij  34337  plymulx  34525  elmrsubrn  35488  faclim  35708  ptrest  37579  poimirlem19  37599  poimirlem20  37600  poimirlem30  37610  ovoliunnfl  37622  voliunnfl  37624  mbfposadd  37627  dvtan  37630  itg2addnclem  37631  ibladdnclem  37636  itgaddnclem1  37638  iblabsnclem  37643  itggt0cn  37650  ftc1anclem4  37656  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  dvasin  37664  dvacos  37665  areacirclem1  37668  aks6d1c1p5  42069  arearect  43176  areaquad  43177  cantnfresb  43286  mptrcllem  43575  dfrcl2  43636  dfrcl3  43637  dftrcl3  43682  dfrtrcl3  43695  dfrtrcl4  43700  lhe4.4ex1a  44298  binomcxplemrat  44319  rnsnf  45091  feqresmptf  45138  limsupresre  45617  limsupvaluzmpt  45638  limsup10ex  45694  liminf10ex  45695  dvnprodlem1  45867  itgsin0pilem1  45871  wallispilem4  45989  wallispi2  45994  stirlinglem1  45995  stirlinglem3  45997  dirkercncflem2  46025  fourierdlem48  46075  fourierdlem49  46076  fourierdlem56  46083  fourierdlem57  46084  fourierdlem58  46085  fourierdlem62  46089  fourierdlem107  46134  fouriersw  46152  etransclem46  46201  sge0tsms  46301  sge0less  46313  sge0iun  46340  meadjun  46383  ovn02  46489  hoidmv1le  46515  hspmbllem2  46548  smflimsuplem3  46743  ackval1  48415  ackval2  48416  ackval3  48417