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 1547	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

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

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 5158  df-mpt 5177

This theorem is referenced by:  mpteq2i  5191  partfun  6633  feqresmpt  6896  elfvmptrab  6963  fmptap  7110  offres  7925  resixpfo  8870  dfoi  9422  cantnflem1d  9603  cantnflem1  9604  dfceil2  13762  dfid5  14953  dfid6  14954  cnrecnv  15091  ackbijnn  15754  harmonic  15785  ege2le3  16016  eirrlem  16132  prmrec  16853  imasdsval2  17439  dfinito2  17929  dftermo2  17930  dfinito3  17931  dftermo3  17932  smndex1iidm  18794  smndex2dlinvh  18810  cayleylem1  19310  pmtrprfval  19385  gsumzsplit  19825  gsum2dlem2  19869  dmdprdsplitlem  19937  frlmip  21704  coe1sclmul  22185  coe1sclmul2  22187  mdetunilem9  22524  leordtvallem1  23114  leordtvallem2  23115  txkgen  23556  cnmpt1st  23572  cnmpt2nd  23573  tmdgsum  23999  tsmssplit  24056  cnfldnm  24683  expcn  24780  expcnOLD  24782  pcorev2  24945  pi1xfrcnv  24974  rrxip  25307  mbfi1flim  25641  itg2uba  25661  itg2cnlem1  25679  itg2cnlem2  25680  itgitg2  25725  itgss3  25733  itgless  25735  ibladdlem  25738  itgaddlem1  25741  iblabslem  25746  itggt0  25762  itgcn  25763  limcdif  25794  limcres  25804  cnplimc  25805  dvcobr  25866  dvcobrOLD  25867  dvexp  25874  dveflem  25900  dvef  25901  dvlip  25915  dvlipcn  25916  lhop  25938  tdeglem2  25983  plyid  26131  coeidp  26186  dgrid  26187  pserdvlem2  26355  abelth  26368  dvrelog  26563  logcn  26573  dvlog  26577  advlog  26580  advlogexp  26581  logtayl  26586  logccv  26589  dvcxp1  26666  dvsqrt  26668  dvcncxp1  26669  dvcnsqrt  26670  resqrtcn  26676  loglesqrt  26688  logblog  26719  dvatan  26862  leibpilem2  26868  leibpi  26869  efrlim  26896  efrlimOLD  26897  sqrtlim  26900  amgmlem  26917  emcllem5  26927  lgamgulmlem2  26957  lgam1  26991  chtublem  27139  logfacrlim2  27154  bposlem6  27217  chto1lb  27406  vmadivsum  27410  dchrvmasumlema  27428  mulogsumlem  27459  logdivsum  27461  logsqvma2  27471  log2sumbnd  27472  selberglem1  27473  selberglem3  27475  selberg  27476  selberg2lem  27478  selberg2  27479  pntrmax  27492  pntrsumo1  27493  selbergr  27496  selbergs  27502  pnt2  27541  pnt  27542  ostth2  27565  ostth  27567  hilnormi  31126  bra0  31913  zrhre  34005  qqhre  34006  eulerpartgbij  34359  plymulx  34535  elmrsubrn  35512  faclim  35738  ptrest  37618  poimirlem19  37638  poimirlem20  37639  poimirlem30  37649  ovoliunnfl  37661  voliunnfl  37663  mbfposadd  37666  dvtan  37669  itg2addnclem  37670  ibladdnclem  37675  itgaddnclem1  37677  iblabsnclem  37682  itggt0cn  37689  ftc1anclem4  37695  ftc1anclem5  37696  ftc1anclem6  37697  ftc1anclem7  37698  ftc1anclem8  37699  dvasin  37703  dvacos  37704  areacirclem1  37707  aks6d1c1p5  42105  redvmptabs  42353  readvrec2  42354  readvrec  42355  readvcot  42357  arearect  43208  areaquad  43209  cantnfresb  43317  mptrcllem  43606  dfrcl2  43667  dfrcl3  43668  dftrcl3  43713  dfrtrcl3  43726  dfrtrcl4  43731  lhe4.4ex1a  44322  binomcxplemrat  44343  rnsnf  45182  feqresmptf  45229  limsupresre  45697  limsupvaluzmpt  45718  limsup10ex  45774  liminf10ex  45775  dvnprodlem1  45947  itgsin0pilem1  45951  wallispilem4  46069  wallispi2  46074  stirlinglem1  46075  stirlinglem3  46077  dirkercncflem2  46105  fourierdlem48  46155  fourierdlem49  46156  fourierdlem56  46163  fourierdlem57  46164  fourierdlem58  46165  fourierdlem62  46169  fourierdlem107  46214  fouriersw  46232  etransclem46  46281  sge0tsms  46381  sge0less  46393  sge0iun  46420  meadjun  46463  ovn02  46569  hoidmv1le  46595  hspmbllem2  46628  smflimsuplem3  46823  ackval1  48686  ackval2  48687  ackval3  48688  dftermo4  49507