Theorem mpteq2ia 5194

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

Syntax hints:   → wi 4   = wceq 1542  ⊤wtru 1543   ∈ wcel 2114   ↦ cmpt 5180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5162  df-mpt 5181

This theorem is referenced by:  mpteq2i  5195  partfun  6640  feqresmpt  6904  elfvmptrab  6972  fmptap  7118  offres  7929  resixpfo  8878  dfoi  9420  cantnflem1d  9601  cantnflem1  9602  dfceil2  13763  dfid5  14954  dfid6  14955  cnrecnv  15092  ackbijnn  15755  harmonic  15786  ege2le3  16017  eirrlem  16133  prmrec  16854  imasdsval2  17441  dfinito2  17931  dftermo2  17932  dfinito3  17933  dftermo3  17934  smndex1iidm  18830  smndex2dlinvh  18846  cayleylem1  19345  pmtrprfval  19420  gsumzsplit  19860  gsum2dlem2  19904  dmdprdsplitlem  19972  frlmip  21737  coe1sclmul  22228  coe1sclmul2  22230  mdetunilem9  22568  leordtvallem1  23158  leordtvallem2  23159  txkgen  23600  cnmpt1st  23616  cnmpt2nd  23617  tmdgsum  24043  tsmssplit  24100  cnfldnm  24726  expcn  24823  expcnOLD  24825  pcorev2  24988  pi1xfrcnv  25017  rrxip  25350  mbfi1flim  25684  itg2uba  25704  itg2cnlem1  25722  itg2cnlem2  25723  itgitg2  25768  itgss3  25776  itgless  25778  ibladdlem  25781  itgaddlem1  25784  iblabslem  25789  itggt0  25805  itgcn  25806  limcdif  25837  limcres  25847  cnplimc  25848  dvcobr  25909  dvcobrOLD  25910  dvexp  25917  dveflem  25943  dvef  25944  dvlip  25958  dvlipcn  25959  lhop  25981  tdeglem2  26026  plyid  26174  coeidp  26229  dgrid  26230  pserdvlem2  26398  abelth  26411  dvrelog  26606  logcn  26616  dvlog  26620  advlog  26623  advlogexp  26624  logtayl  26629  logccv  26632  dvcxp1  26709  dvsqrt  26711  dvcncxp1  26712  dvcnsqrt  26713  resqrtcn  26719  loglesqrt  26731  logblog  26762  dvatan  26905  leibpilem2  26911  leibpi  26912  efrlim  26939  efrlimOLD  26940  sqrtlim  26943  amgmlem  26960  emcllem5  26970  lgamgulmlem2  27000  lgam1  27034  chtublem  27182  logfacrlim2  27197  bposlem6  27260  chto1lb  27449  vmadivsum  27453  dchrvmasumlema  27471  mulogsumlem  27502  logdivsum  27504  logsqvma2  27514  log2sumbnd  27515  selberglem1  27516  selberglem3  27518  selberg  27519  selberg2lem  27521  selberg2  27522  pntrmax  27535  pntrsumo1  27536  selbergr  27539  selbergs  27545  pnt2  27584  pnt  27585  ostth2  27608  ostth  27610  hilnormi  31221  bra0  32008  partfun2  32736  zrhre  34157  qqhre  34158  eulerpartgbij  34510  plymulx  34686  elmrsubrn  35695  faclim  35921  ptrest  37791  poimirlem19  37811  poimirlem20  37812  poimirlem30  37822  ovoliunnfl  37834  voliunnfl  37836  mbfposadd  37839  dvtan  37842  itg2addnclem  37843  ibladdnclem  37848  itgaddnclem1  37850  iblabsnclem  37855  itggt0cn  37862  ftc1anclem4  37868  ftc1anclem5  37869  ftc1anclem6  37870  ftc1anclem7  37871  ftc1anclem8  37872  dvasin  37876  dvacos  37877  areacirclem1  37880  dfadjliftmap2  38629  dfblockliftmap2  38633  aks6d1c1p5  42403  redvmptabs  42651  readvrec2  42652  readvrec  42653  readvcot  42655  arearect  43493  areaquad  43494  cantnfresb  43602  mptrcllem  43890  dfrcl2  43951  dfrcl3  43952  dftrcl3  43997  dfrtrcl3  44010  dfrtrcl4  44015  lhe4.4ex1a  44606  binomcxplemrat  44627  rnsnf  45464  feqresmptf  45511  limsupresre  45976  limsupvaluzmpt  45997  limsup10ex  46053  liminf10ex  46054  dvnprodlem1  46226  itgsin0pilem1  46230  wallispilem4  46348  wallispi2  46353  stirlinglem1  46354  stirlinglem3  46356  dirkercncflem2  46384  fourierdlem48  46434  fourierdlem49  46435  fourierdlem56  46442  fourierdlem57  46443  fourierdlem58  46444  fourierdlem62  46448  fourierdlem107  46493  fouriersw  46511  etransclem46  46560  sge0tsms  46660  sge0less  46672  sge0iun  46699  meadjun  46742  ovn02  46848  hoidmv1le  46874  hspmbllem2  46907  smflimsuplem3  47102  ackval1  48963  ackval2  48964  ackval3  48965  dftermo4  49783