Theorem mpteq2ia 5200

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 487	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	mpteq2dva 5198	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
4	3	mptru 1577	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⊤wtru 1571   ∈ wcel 2145   ↦ cmpt 5186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-mpt 5187

This theorem is used by:  mpteq2i  5201  partfun  6684  feqresmpt  6952  elfvmptrab  7021  fmptap  7173  offres  7993  resixpfo  8957  dfoi  9498  cantnflem1d  9682  cantnflem1  9683  dfceil2  13972  dfid5  15173  dfid6  15174  cnrecnv  15325  ackbijnn  15990  harmonic  16021  ege2le3  16249  eirrlem  16365  prmrec  17093  imasdsval2  17681  dfinito2  18171  dftermo2  18172  dfinito3  18173  dftermo3  18174  smndex1iidm  19090  smndex2dlinvh  19109  cayleylem1  19619  pmtrprfval  19694  gsumzsplit  20134  gsum2dlem2  20178  dmdprdsplitlem  20246  frlmip  22077  coe1sclmul  22594  coe1sclmul2  22596  mdetunilem9  22928  leordtvallem1  23521  leordtvallem2  23522  txkgen  23964  cnmpt1st  23980  cnmpt2nd  23981  tmdgsum  24407  tsmssplit  24464  cnfldnm  25090  expcn  25186  pcorev2  25342  pi1xfrcnv  25371  rrxip  25704  mbfi1flim  26037  itg2uba  26057  itg2cnlem1  26075  itg2cnlem2  26076  itgitg2  26120  itgss3  26128  itgless  26130  ibladdlem  26133  itgaddlem1  26136  iblabslem  26141  itggt0  26157  itgcn  26158  limcdif  26189  limcres  26199  cnplimc  26200  dvcobr  26259  dvexp  26266  dveflem  26292  dvef  26293  dvlip  26306  dvlipcn  26307  lhop  26329  tdeglem2  26372  plyid  26520  coeidp  26575  dgrid  26576  plymulidp  26596  pserdvlem2  26748  abelth  26761  dvrelog  26958  logcn  26968  dvlog  26972  advlog  26975  advlogexp  26976  logtayl  26981  logccv  26984  dvcxp1  27061  dvsqrt  27063  dvcncxp1  27064  dvcnsqrt  27065  resqrtcn  27070  loglesqrt  27082  logblog  27113  dvatan  27256  leibpilem2  27262  leibpi  27263  efrlim  27290  sqrtlim  27293  amgmlem  27310  emcllem5  27320  lgamgulmlem2  27350  lgam1  27384  chtublem  27531  logfacrlim2  27546  bposlem6  27609  chto1lb  27798  vmadivsum  27802  dchrvmasumlema  27820  mulogsumlem  27851  logdivsum  27853  logsqvma2  27863  log2sumbnd  27864  selberglem1  27865  selberglem3  27867  selberg  27868  selberg2lem  27870  selberg2  27871  pntrmax  27884  pntrsumo1  27885  selbergr  27888  selbergs  27894  pnt2  27933  pnt  27934  ostth2  27957  ostth  27959  hilnormi  31758  bra0  32545  partfun2  33263  mplmonprod  34179  zrhre  34644  qqhre  34645  eulerpartgbij  34997  elmrsubrn  36264  faclim  36490  ptrest  38517  poimirlem19  38537  poimirlem20  38538  poimirlem30  38548  ovoliunnfl  38560  voliunnfl  38562  mbfposadd  38565  dvtan  38568  itg2addnclem  38569  ibladdnclem  38574  itgaddnclem1  38576  iblabsnclem  38581  itggt0cn  38588  ftc1anclem4  38594  ftc1anclem5  38595  ftc1anclem6  38596  ftc1anclem7  38597  ftc1anclem8  38598  dvasin  38602  dvacos  38603  areacirclem1  38606  dfadjliftmap2  39369  dfblockliftmap2  39373  aks6d1c1p5  43142  redvmptabs  43391  readvrec2  43392  readvrec  43393  readvcot  43395  arearect  44201  areaquad  44202  cantnfresb  44310  mptrcllem  44598  dfrcl2  44659  dfrcl3  44660  dftrcl3  44705  dfrtrcl3  44718  dfrtrcl4  44723  lhe4.4ex1a  45298  binomcxplemrat  45319  rnsnf  46168  feqresmptf  46212  limsupresre  46675  limsupvaluzmpt  46696  limsup10ex  46752  liminf10ex  46753  dvnprodlem1  46925  itgsin0pilem1  46929  wallispilem4  47047  wallispi2  47052  stirlinglem1  47053  stirlinglem3  47055  dirkercncflem2  47083  fourierdlem48  47133  fourierdlem49  47134  fourierdlem56  47141  fourierdlem57  47142  fourierdlem58  47143  fourierdlem62  47147  fourierdlem107  47192  fouriersw  47210  etransclem46  47259  sge0tsms  47359  sge0less  47371  sge0iun  47398  meadjun  47441  ovn02  47547  hoidmv1le  47573  hspmbllem2  47606  smflimsuplem3  47801  sqrtnpoly  47912  indprm  48683  indprmfz  48684  ackval1  49762  ackval2  49763  ackval3  49764  dftermo4  50579  dvsec  50825  dvcsc  50826  dvcot  50827