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 2732

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

This theorem is used by:  mpteq2i  5201  partfun  6679  feqresmpt  6947  elfvmptrab  7016  fmptap  7168  offres  7980  resixpfo  8943  dfoi  9483  cantnflem1d  9667  cantnflem1  9668  dfceil2  13900  dfid5  15100  dfid6  15101  cnrecnv  15252  ackbijnn  15917  harmonic  15948  ege2le3  16176  eirrlem  16292  prmrec  17014  imasdsval2  17602  dfinito2  18092  dftermo2  18093  dfinito3  18094  dftermo3  18095  smndex1iidm  19010  smndex2dlinvh  19029  cayleylem1  19539  pmtrprfval  19614  gsumzsplit  20054  gsum2dlem2  20098  dmdprdsplitlem  20166  frlmip  21991  coe1sclmul  22508  coe1sclmul2  22510  mdetunilem9  22842  leordtvallem1  23435  leordtvallem2  23436  txkgen  23878  cnmpt1st  23894  cnmpt2nd  23895  tmdgsum  24321  tsmssplit  24378  cnfldnm  25004  expcn  25100  pcorev2  25256  pi1xfrcnv  25285  rrxip  25618  mbfi1flim  25951  itg2uba  25971  itg2cnlem1  25989  itg2cnlem2  25990  itgitg2  26034  itgss3  26042  itgless  26044  ibladdlem  26047  itgaddlem1  26050  iblabslem  26055  itggt0  26071  itgcn  26072  limcdif  26103  limcres  26113  cnplimc  26114  dvcobr  26173  dvexp  26180  dveflem  26206  dvef  26207  dvlip  26220  dvlipcn  26221  lhop  26243  tdeglem2  26286  plyid  26434  coeidp  26489  dgrid  26490  plymulidp  26512  pserdvlem2  26664  abelth  26677  dvrelog  26874  logcn  26884  dvlog  26888  advlog  26891  advlogexp  26892  logtayl  26897  logccv  26900  dvcxp1  26977  dvsqrt  26979  dvcncxp1  26980  dvcnsqrt  26981  resqrtcn  26986  loglesqrt  26998  logblog  27029  dvatan  27172  leibpilem2  27178  leibpi  27179  efrlim  27206  sqrtlim  27209  amgmlem  27226  emcllem5  27236  lgamgulmlem2  27266  lgam1  27300  chtublem  27447  logfacrlim2  27462  bposlem6  27525  chto1lb  27714  vmadivsum  27718  dchrvmasumlema  27736  mulogsumlem  27767  logdivsum  27769  logsqvma2  27779  log2sumbnd  27780  selberglem1  27781  selberglem3  27783  selberg  27784  selberg2lem  27786  selberg2  27787  pntrmax  27800  pntrsumo1  27801  selbergr  27804  selbergs  27810  pnt2  27849  pnt  27850  ostth2  27873  ostth  27875  hilnormi  31644  bra0  32431  partfun2  33149  mplmonprod  34064  zrhre  34529  qqhre  34530  eulerpartgbij  34883  elmrsubrn  36099  faclim  36325  ptrest  38368  poimirlem19  38388  poimirlem20  38389  poimirlem30  38399  ovoliunnfl  38411  voliunnfl  38413  mbfposadd  38416  dvtan  38419  itg2addnclem  38420  ibladdnclem  38425  itgaddnclem1  38427  iblabsnclem  38432  itggt0cn  38439  ftc1anclem4  38445  ftc1anclem5  38446  ftc1anclem6  38447  ftc1anclem7  38448  ftc1anclem8  38449  dvasin  38453  dvacos  38454  areacirclem1  38457  dfadjliftmap2  39205  dfblockliftmap2  39209  aks6d1c1p5  42978  redvmptabs  43235  readvrec2  43236  readvrec  43237  readvcot  43239  arearect  44056  areaquad  44057  cantnfresb  44165  mptrcllem  44453  dfrcl2  44514  dfrcl3  44515  dftrcl3  44560  dfrtrcl3  44573  dfrtrcl4  44578  lhe4.4ex1a  45153  binomcxplemrat  45174  rnsnf  46016  feqresmptf  46060  limsupresre  46524  limsupvaluzmpt  46545  limsup10ex  46601  liminf10ex  46602  dvnprodlem1  46774  itgsin0pilem1  46778  wallispilem4  46896  wallispi2  46901  stirlinglem1  46902  stirlinglem3  46904  dirkercncflem2  46932  fourierdlem48  46982  fourierdlem49  46983  fourierdlem56  46990  fourierdlem57  46991  fourierdlem58  46992  fourierdlem62  46996  fourierdlem107  47041  fouriersw  47059  etransclem46  47108  sge0tsms  47208  sge0less  47220  sge0iun  47247  meadjun  47290  ovn02  47396  hoidmv1le  47422  hspmbllem2  47455  smflimsuplem3  47650  sqrtnpoly  47761  indprm  48532  indprmfz  48533  ackval1  49611  ackval2  49612  ackval3  49613  dftermo4  50428  dvsec  50689  dvcsc  50690  dvcot  50691