Theorem mpteq2ia 5190

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

Syntax hints:   → wi 4   = wceq 1541  ⊤wtru 1542   ∈ wcel 2113   ↦ cmpt 5176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-opab 5158  df-mpt 5177

This theorem is referenced by:  mpteq2i  5191  partfun  6636  feqresmpt  6900  elfvmptrab  6967  fmptap  7113  offres  7924  resixpfo  8870  dfoi  9408  cantnflem1d  9589  cantnflem1  9590  dfceil2  13750  dfid5  14941  dfid6  14942  cnrecnv  15079  ackbijnn  15742  harmonic  15773  ege2le3  16004  eirrlem  16120  prmrec  16841  imasdsval2  17428  dfinito2  17918  dftermo2  17919  dfinito3  17920  dftermo3  17921  smndex1iidm  18817  smndex2dlinvh  18833  cayleylem1  19332  pmtrprfval  19407  gsumzsplit  19847  gsum2dlem2  19891  dmdprdsplitlem  19959  frlmip  21724  coe1sclmul  22215  coe1sclmul2  22217  mdetunilem9  22555  leordtvallem1  23145  leordtvallem2  23146  txkgen  23587  cnmpt1st  23603  cnmpt2nd  23604  tmdgsum  24030  tsmssplit  24087  cnfldnm  24713  expcn  24810  expcnOLD  24812  pcorev2  24975  pi1xfrcnv  25004  rrxip  25337  mbfi1flim  25671  itg2uba  25691  itg2cnlem1  25709  itg2cnlem2  25710  itgitg2  25755  itgss3  25763  itgless  25765  ibladdlem  25768  itgaddlem1  25771  iblabslem  25776  itggt0  25792  itgcn  25793  limcdif  25824  limcres  25834  cnplimc  25835  dvcobr  25896  dvcobrOLD  25897  dvexp  25904  dveflem  25930  dvef  25931  dvlip  25945  dvlipcn  25946  lhop  25968  tdeglem2  26013  plyid  26161  coeidp  26216  dgrid  26217  pserdvlem2  26385  abelth  26398  dvrelog  26593  logcn  26603  dvlog  26607  advlog  26610  advlogexp  26611  logtayl  26616  logccv  26619  dvcxp1  26696  dvsqrt  26698  dvcncxp1  26699  dvcnsqrt  26700  resqrtcn  26706  loglesqrt  26718  logblog  26749  dvatan  26892  leibpilem2  26898  leibpi  26899  efrlim  26926  efrlimOLD  26927  sqrtlim  26930  amgmlem  26947  emcllem5  26957  lgamgulmlem2  26987  lgam1  27021  chtublem  27169  logfacrlim2  27184  bposlem6  27247  chto1lb  27436  vmadivsum  27440  dchrvmasumlema  27458  mulogsumlem  27489  logdivsum  27491  logsqvma2  27501  log2sumbnd  27502  selberglem1  27503  selberglem3  27505  selberg  27506  selberg2lem  27508  selberg2  27509  pntrmax  27522  pntrsumo1  27523  selbergr  27526  selbergs  27532  pnt2  27571  pnt  27572  ostth2  27595  ostth  27597  hilnormi  31164  bra0  31951  partfun2  32681  zrhre  34104  qqhre  34105  eulerpartgbij  34457  plymulx  34633  elmrsubrn  35636  faclim  35862  ptrest  37732  poimirlem19  37752  poimirlem20  37753  poimirlem30  37763  ovoliunnfl  37775  voliunnfl  37777  mbfposadd  37780  dvtan  37783  itg2addnclem  37784  ibladdnclem  37789  itgaddnclem1  37791  iblabsnclem  37796  itggt0cn  37803  ftc1anclem4  37809  ftc1anclem5  37810  ftc1anclem6  37811  ftc1anclem7  37812  ftc1anclem8  37813  dvasin  37817  dvacos  37818  areacirclem1  37821  dfadjliftmap2  38544  dfblockliftmap2  38547  aks6d1c1p5  42278  redvmptabs  42530  readvrec2  42531  readvrec  42532  readvcot  42534  arearect  43372  areaquad  43373  cantnfresb  43481  mptrcllem  43770  dfrcl2  43831  dfrcl3  43832  dftrcl3  43877  dfrtrcl3  43890  dfrtrcl4  43895  lhe4.4ex1a  44486  binomcxplemrat  44507  rnsnf  45344  feqresmptf  45391  limsupresre  45856  limsupvaluzmpt  45877  limsup10ex  45933  liminf10ex  45934  dvnprodlem1  46106  itgsin0pilem1  46110  wallispilem4  46228  wallispi2  46233  stirlinglem1  46234  stirlinglem3  46236  dirkercncflem2  46264  fourierdlem48  46314  fourierdlem49  46315  fourierdlem56  46322  fourierdlem57  46323  fourierdlem58  46324  fourierdlem62  46328  fourierdlem107  46373  fouriersw  46391  etransclem46  46440  sge0tsms  46540  sge0less  46552  sge0iun  46579  meadjun  46622  ovn02  46728  hoidmv1le  46754  hspmbllem2  46787  smflimsuplem3  46982  ackval1  48843  ackval2  48844  ackval3  48845  dftermo4  49663