Theorem mpteq2ia 5195

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

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

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 5163  df-mpt 5182

This theorem is referenced by:  mpteq2i  5196  partfun  6647  feqresmpt  6911  elfvmptrab  6979  fmptap  7126  offres  7937  resixpfo  8886  dfoi  9428  cantnflem1d  9609  cantnflem1  9610  dfceil2  13771  dfid5  14962  dfid6  14963  cnrecnv  15100  ackbijnn  15763  harmonic  15794  ege2le3  16025  eirrlem  16141  prmrec  16862  imasdsval2  17449  dfinito2  17939  dftermo2  17940  dfinito3  17941  dftermo3  17942  smndex1iidm  18838  smndex2dlinvh  18854  cayleylem1  19353  pmtrprfval  19428  gsumzsplit  19868  gsum2dlem2  19912  dmdprdsplitlem  19980  frlmip  21745  coe1sclmul  22236  coe1sclmul2  22238  mdetunilem9  22576  leordtvallem1  23166  leordtvallem2  23167  txkgen  23608  cnmpt1st  23624  cnmpt2nd  23625  tmdgsum  24051  tsmssplit  24108  cnfldnm  24734  expcn  24831  expcnOLD  24833  pcorev2  24996  pi1xfrcnv  25025  rrxip  25358  mbfi1flim  25692  itg2uba  25712  itg2cnlem1  25730  itg2cnlem2  25731  itgitg2  25776  itgss3  25784  itgless  25786  ibladdlem  25789  itgaddlem1  25792  iblabslem  25797  itggt0  25813  itgcn  25814  limcdif  25845  limcres  25855  cnplimc  25856  dvcobr  25917  dvcobrOLD  25918  dvexp  25925  dveflem  25951  dvef  25952  dvlip  25966  dvlipcn  25967  lhop  25989  tdeglem2  26034  plyid  26182  coeidp  26237  dgrid  26238  pserdvlem2  26406  abelth  26419  dvrelog  26614  logcn  26624  dvlog  26628  advlog  26631  advlogexp  26632  logtayl  26637  logccv  26640  dvcxp1  26717  dvsqrt  26719  dvcncxp1  26720  dvcnsqrt  26721  resqrtcn  26727  loglesqrt  26739  logblog  26770  dvatan  26913  leibpilem2  26919  leibpi  26920  efrlim  26947  efrlimOLD  26948  sqrtlim  26951  amgmlem  26968  emcllem5  26978  lgamgulmlem2  27008  lgam1  27042  chtublem  27190  logfacrlim2  27205  bposlem6  27268  chto1lb  27457  vmadivsum  27461  dchrvmasumlema  27479  mulogsumlem  27510  logdivsum  27512  logsqvma2  27522  log2sumbnd  27523  selberglem1  27524  selberglem3  27526  selberg  27527  selberg2lem  27529  selberg2  27530  pntrmax  27543  pntrsumo1  27544  selbergr  27547  selbergs  27553  pnt2  27592  pnt  27593  ostth2  27616  ostth  27618  hilnormi  31251  bra0  32038  partfun2  32766  mplmonprod  33731  zrhre  34197  qqhre  34198  eulerpartgbij  34550  plymulx  34726  elmrsubrn  35736  faclim  35962  ptrest  37870  poimirlem19  37890  poimirlem20  37891  poimirlem30  37901  ovoliunnfl  37913  voliunnfl  37915  mbfposadd  37918  dvtan  37921  itg2addnclem  37922  ibladdnclem  37927  itgaddnclem1  37929  iblabsnclem  37934  itggt0cn  37941  ftc1anclem4  37947  ftc1anclem5  37948  ftc1anclem6  37949  ftc1anclem7  37950  ftc1anclem8  37951  dvasin  37955  dvacos  37956  areacirclem1  37959  dfadjliftmap2  38708  dfblockliftmap2  38712  aks6d1c1p5  42482  redvmptabs  42730  readvrec2  42731  readvrec  42732  readvcot  42734  arearect  43572  areaquad  43573  cantnfresb  43681  mptrcllem  43969  dfrcl2  44030  dfrcl3  44031  dftrcl3  44076  dfrtrcl3  44089  dfrtrcl4  44094  lhe4.4ex1a  44685  binomcxplemrat  44706  rnsnf  45543  feqresmptf  45589  limsupresre  46054  limsupvaluzmpt  46075  limsup10ex  46131  liminf10ex  46132  dvnprodlem1  46304  itgsin0pilem1  46308  wallispilem4  46426  wallispi2  46431  stirlinglem1  46432  stirlinglem3  46434  dirkercncflem2  46462  fourierdlem48  46512  fourierdlem49  46513  fourierdlem56  46520  fourierdlem57  46521  fourierdlem58  46522  fourierdlem62  46526  fourierdlem107  46571  fouriersw  46589  etransclem46  46638  sge0tsms  46738  sge0less  46750  sge0iun  46777  meadjun  46820  ovn02  46926  hoidmv1le  46952  hspmbllem2  46985  smflimsuplem3  47180  ackval1  49041  ackval2  49042  ackval3  49043  dftermo4  49861