Theorem mpteq2ia 5173

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-opab 5133  df-mpt 5154

This theorem is referenced by:  mpteq2i  5175  partfun  6564  feqresmpt  6820  elfvmptrab  6885  fmptap  7024  offres  7799  resixpfo  8682  dfoi  9200  cantnflem1d  9376  cantnflem1  9377  dfceil2  13487  dfid5  14666  dfid6  14667  cnrecnv  14804  ackbijnn  15468  harmonic  15499  ege2le3  15727  eirrlem  15841  prmrec  16551  imasdsval2  17144  dfinito2  17634  dftermo2  17635  dfinito3  17636  dftermo3  17637  smndex1iidm  18455  smndex2dlinvh  18471  cayleylem1  18935  pmtrprfval  19010  gsumzsplit  19443  gsum2dlem2  19487  dmdprdsplitlem  19555  frlmip  20895  coe1sclmul  21363  coe1sclmul2  21365  mdetunilem9  21677  leordtvallem1  22269  leordtvallem2  22270  txkgen  22711  cnmpt1st  22727  cnmpt2nd  22728  tmdgsum  23154  tsmssplit  23211  cnfldnm  23848  expcn  23941  pcorev2  24097  pi1xfrcnv  24126  rrxip  24459  mbfi1flim  24793  itg2uba  24813  itg2cnlem1  24831  itg2cnlem2  24832  itgitg2  24876  itgss3  24884  itgless  24886  ibladdlem  24889  itgaddlem1  24892  iblabslem  24897  itggt0  24913  itgcn  24914  limcdif  24945  limcres  24955  cnplimc  24956  dvcobr  25015  dvexp  25022  dveflem  25048  dvef  25049  dvlip  25062  dvlipcn  25063  lhop  25085  tdeglem2  25131  plyid  25275  coeidp  25329  dgrid  25330  pserdvlem2  25492  abelth  25505  dvrelog  25697  logcn  25707  dvlog  25711  advlog  25714  advlogexp  25715  logtayl  25720  logccv  25723  dvcxp1  25798  dvsqrt  25800  dvcncxp1  25801  dvcnsqrt  25802  resqrtcn  25807  loglesqrt  25816  logblog  25847  dvatan  25990  leibpilem2  25996  leibpi  25997  efrlim  26024  sqrtlim  26027  amgmlem  26044  emcllem5  26054  lgamgulmlem2  26084  lgam1  26118  chtublem  26264  logfacrlim2  26279  bposlem6  26342  chto1lb  26531  vmadivsum  26535  dchrvmasumlema  26553  mulogsumlem  26584  logdivsum  26586  logsqvma2  26596  log2sumbnd  26597  selberglem1  26598  selberglem3  26600  selberg  26601  selberg2lem  26603  selberg2  26604  pntrmax  26617  pntrsumo1  26618  selbergr  26621  selbergs  26627  pnt2  26666  pnt  26667  ostth2  26690  ostth  26692  hilnormi  29426  bra0  30213  zrhre  31869  qqhre  31870  eulerpartgbij  32239  plymulx  32427  elmrsubrn  33382  faclim  33618  ptrest  35703  poimirlem19  35723  poimirlem20  35724  poimirlem30  35734  ovoliunnfl  35746  voliunnfl  35748  mbfposadd  35751  dvtan  35754  itg2addnclem  35755  ibladdnclem  35760  itgaddnclem1  35762  iblabsnclem  35767  itggt0cn  35774  ftc1anclem4  35780  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  dvasin  35788  dvacos  35789  areacirclem1  35792  arearect  40962  areaquad  40963  mptrcllem  41110  dfrcl2  41171  dfrcl3  41172  dftrcl3  41217  dfrtrcl3  41230  dfrtrcl4  41235  lhe4.4ex1a  41836  binomcxplemrat  41857  rnsnf  42610  feqresmptf  42661  limsupresre  43127  limsupvaluzmpt  43148  limsup10ex  43204  liminf10ex  43205  dvnprodlem1  43377  itgsin0pilem1  43381  wallispilem4  43499  wallispi2  43504  stirlinglem1  43505  stirlinglem3  43507  dirkercncflem2  43535  fourierdlem48  43585  fourierdlem49  43586  fourierdlem56  43593  fourierdlem57  43594  fourierdlem58  43595  fourierdlem62  43599  fourierdlem107  43644  fouriersw  43662  etransclem46  43711  sge0tsms  43808  sge0less  43820  sge0iun  43847  meadjun  43890  ovn02  43996  hoidmv1le  44022  hspmbllem2  44055  smflimsuplem3  44242  ackval1  45915  ackval2  45916  ackval3  45917