Theorem mpteq2ia 5197

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

Syntax hints:   → wi 4   = wceq 1540  ⊤wtru 1541   ∈ wcel 2109   ↦ cmpt 5183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5165  df-mpt 5184

This theorem is referenced by:  mpteq2i  5198  partfun  6647  feqresmpt  6912  elfvmptrab  6979  fmptap  7126  offres  7941  resixpfo  8886  dfoi  9440  cantnflem1d  9617  cantnflem1  9618  dfceil2  13777  dfid5  14969  dfid6  14970  cnrecnv  15107  ackbijnn  15770  harmonic  15801  ege2le3  16032  eirrlem  16148  prmrec  16869  imasdsval2  17455  dfinito2  17941  dftermo2  17942  dfinito3  17943  dftermo3  17944  smndex1iidm  18804  smndex2dlinvh  18820  cayleylem1  19318  pmtrprfval  19393  gsumzsplit  19833  gsum2dlem2  19877  dmdprdsplitlem  19945  frlmip  21663  coe1sclmul  22144  coe1sclmul2  22146  mdetunilem9  22483  leordtvallem1  23073  leordtvallem2  23074  txkgen  23515  cnmpt1st  23531  cnmpt2nd  23532  tmdgsum  23958  tsmssplit  24015  cnfldnm  24642  expcn  24739  expcnOLD  24741  pcorev2  24904  pi1xfrcnv  24933  rrxip  25266  mbfi1flim  25600  itg2uba  25620  itg2cnlem1  25638  itg2cnlem2  25639  itgitg2  25684  itgss3  25692  itgless  25694  ibladdlem  25697  itgaddlem1  25700  iblabslem  25705  itggt0  25721  itgcn  25722  limcdif  25753  limcres  25763  cnplimc  25764  dvcobr  25825  dvcobrOLD  25826  dvexp  25833  dveflem  25859  dvef  25860  dvlip  25874  dvlipcn  25875  lhop  25897  tdeglem2  25942  plyid  26090  coeidp  26145  dgrid  26146  pserdvlem2  26314  abelth  26327  dvrelog  26522  logcn  26532  dvlog  26536  advlog  26539  advlogexp  26540  logtayl  26545  logccv  26548  dvcxp1  26625  dvsqrt  26627  dvcncxp1  26628  dvcnsqrt  26629  resqrtcn  26635  loglesqrt  26647  logblog  26678  dvatan  26821  leibpilem2  26827  leibpi  26828  efrlim  26855  efrlimOLD  26856  sqrtlim  26859  amgmlem  26876  emcllem5  26886  lgamgulmlem2  26916  lgam1  26950  chtublem  27098  logfacrlim2  27113  bposlem6  27176  chto1lb  27365  vmadivsum  27369  dchrvmasumlema  27387  mulogsumlem  27418  logdivsum  27420  logsqvma2  27430  log2sumbnd  27431  selberglem1  27432  selberglem3  27434  selberg  27435  selberg2lem  27437  selberg2  27438  pntrmax  27451  pntrsumo1  27452  selbergr  27455  selbergs  27461  pnt2  27500  pnt  27501  ostth2  27524  ostth  27526  hilnormi  31065  bra0  31852  zrhre  33982  qqhre  33983  eulerpartgbij  34336  plymulx  34512  elmrsubrn  35480  faclim  35706  ptrest  37586  poimirlem19  37606  poimirlem20  37607  poimirlem30  37617  ovoliunnfl  37629  voliunnfl  37631  mbfposadd  37634  dvtan  37637  itg2addnclem  37638  ibladdnclem  37643  itgaddnclem1  37645  iblabsnclem  37650  itggt0cn  37657  ftc1anclem4  37663  ftc1anclem5  37664  ftc1anclem6  37665  ftc1anclem7  37666  ftc1anclem8  37667  dvasin  37671  dvacos  37672  areacirclem1  37675  aks6d1c1p5  42073  redvmptabs  42321  readvrec2  42322  readvrec  42323  readvcot  42325  arearect  43177  areaquad  43178  cantnfresb  43286  mptrcllem  43575  dfrcl2  43636  dfrcl3  43637  dftrcl3  43682  dfrtrcl3  43695  dfrtrcl4  43700  lhe4.4ex1a  44291  binomcxplemrat  44312  rnsnf  45151  feqresmptf  45198  limsupresre  45667  limsupvaluzmpt  45688  limsup10ex  45744  liminf10ex  45745  dvnprodlem1  45917  itgsin0pilem1  45921  wallispilem4  46039  wallispi2  46044  stirlinglem1  46045  stirlinglem3  46047  dirkercncflem2  46075  fourierdlem48  46125  fourierdlem49  46126  fourierdlem56  46133  fourierdlem57  46134  fourierdlem58  46135  fourierdlem62  46139  fourierdlem107  46184  fouriersw  46202  etransclem46  46251  sge0tsms  46351  sge0less  46363  sge0iun  46390  meadjun  46433  ovn02  46539  hoidmv1le  46565  hspmbllem2  46598  smflimsuplem3  46793  ackval1  48643  ackval2  48644  ackval3  48645  dftermo4  49464