Theorem mpteq2ia 5208

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5176  df-mpt 5195

This theorem is used by:  mpteq2i  5209  partfun  6686  feqresmpt  6954  elfvmptrab  7023  fmptap  7172  offres  7982  resixpfo  8936  dfoi  9476  cantnflem1d  9660  cantnflem1  9661  dfceil2  13886  dfid5  15084  dfid6  15085  cnrecnv  15236  ackbijnn  15901  harmonic  15932  ege2le3  16162  eirrlem  16278  prmrec  17000  imasdsval2  17588  dfinito2  18078  dftermo2  18079  dfinito3  18080  dftermo3  18081  smndex1iidm  18984  smndex2dlinvh  19003  cayleylem1  19506  pmtrprfval  19581  gsumzsplit  20021  gsum2dlem2  20065  dmdprdsplitlem  20133  frlmip  21958  coe1sclmul  22473  coe1sclmul2  22475  mdetunilem9  22807  leordtvallem1  23397  leordtvallem2  23398  txkgen  23840  cnmpt1st  23856  cnmpt2nd  23857  tmdgsum  24283  tsmssplit  24340  cnfldnm  24966  expcn  25062  pcorev2  25218  pi1xfrcnv  25247  rrxip  25580  mbfi1flim  25913  itg2uba  25933  itg2cnlem1  25951  itg2cnlem2  25952  itgitg2  25997  itgss3  26005  itgless  26007  ibladdlem  26010  itgaddlem1  26013  iblabslem  26018  itggt0  26034  itgcn  26035  limcdif  26066  limcres  26076  cnplimc  26077  dvcobr  26136  dvexp  26143  dveflem  26169  dvef  26170  dvlip  26183  dvlipcn  26184  lhop  26206  tdeglem2  26249  plyid  26397  coeidp  26451  dgrid  26452  plymulidp  26474  pserdvlem2  26622  abelth  26635  dvrelog  26833  logcn  26843  dvlog  26847  advlog  26850  advlogexp  26851  logtayl  26856  logccv  26859  dvcxp1  26936  dvsqrt  26938  dvcncxp1  26939  dvcnsqrt  26940  resqrtcn  26945  loglesqrt  26957  logblog  26988  dvatan  27131  leibpilem2  27137  leibpi  27138  efrlim  27165  sqrtlim  27168  amgmlem  27185  emcllem5  27195  lgamgulmlem2  27225  lgam1  27259  chtublem  27406  logfacrlim2  27421  bposlem6  27484  chto1lb  27673  vmadivsum  27677  dchrvmasumlema  27695  mulogsumlem  27726  logdivsum  27728  logsqvma2  27738  log2sumbnd  27739  selberglem1  27740  selberglem3  27742  selberg  27743  selberg2lem  27745  selberg2  27746  pntrmax  27759  pntrsumo1  27760  selbergr  27763  selbergs  27769  pnt2  27808  pnt  27809  ostth2  27832  ostth  27834  hilnormi  31562  bra0  32349  partfun2  33068  mplmonprod  33984  zrhre  34449  qqhre  34450  eulerpartgbij  34803  elmrsubrn  36025  faclim  36251  ptrest  38303  poimirlem19  38323  poimirlem20  38324  poimirlem30  38334  ovoliunnfl  38346  voliunnfl  38348  mbfposadd  38351  dvtan  38354  itg2addnclem  38355  ibladdnclem  38360  itgaddnclem1  38362  iblabsnclem  38367  itggt0cn  38374  ftc1anclem4  38380  ftc1anclem5  38381  ftc1anclem6  38382  ftc1anclem7  38383  ftc1anclem8  38384  dvasin  38388  dvacos  38389  areacirclem1  38392  dfadjliftmap2  39139  dfblockliftmap2  39143  aks6d1c1p5  42912  redvmptabs  43154  readvrec2  43155  readvrec  43156  readvcot  43158  arearect  43975  areaquad  43976  cantnfresb  44084  mptrcllem  44372  dfrcl2  44433  dfrcl3  44434  dftrcl3  44479  dfrtrcl3  44492  dfrtrcl4  44497  lhe4.4ex1a  45072  binomcxplemrat  45093  rnsnf  45935  feqresmptf  45979  limsupresre  46443  limsupvaluzmpt  46464  limsup10ex  46520  liminf10ex  46521  dvnprodlem1  46693  itgsin0pilem1  46697  wallispilem4  46815  wallispi2  46820  stirlinglem1  46821  stirlinglem3  46823  dirkercncflem2  46851  fourierdlem48  46901  fourierdlem49  46902  fourierdlem56  46909  fourierdlem57  46910  fourierdlem58  46911  fourierdlem62  46915  fourierdlem107  46960  fouriersw  46978  etransclem46  47027  sge0tsms  47127  sge0less  47139  sge0iun  47166  meadjun  47209  ovn02  47315  hoidmv1le  47341  hspmbllem2  47374  smflimsuplem3  47569  indprm  48414  indprmfz  48415  ackval1  49494  ackval2  49495  ackval3  49496  dftermo4  50313