Theorem mpteq2ia 5204

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5172  df-mpt 5191

This theorem is used by:  mpteq2i  5205  partfun  6714  feqresmpt  6983  elfvmptrab  7052  fmptap  7204  offres  8027  resixpfo  9000  dfoi  9540  cantnflem1d  9724  cantnflem1  9725  dfceil2  14017  dfid5  15221  dfid6  15222  cnrecnv  15373  ackbijnn  16038  harmonic  16069  ege2le3  16297  eirrlem  16413  prmrec  17141  imasdsval2  17729  dfinito2  18219  dftermo2  18220  dfinito3  18221  dftermo3  18222  smndex1iidm  19138  smndex2dlinvh  19157  cayleylem1  19668  pmtrprfval  19743  gsumzsplit  20183  gsum2dlem2  20227  dmdprdsplitlem  20295  frlmip  22128  coe1sclmul  22645  coe1sclmul2  22647  mdetunilem9  22979  leordtvallem1  23572  leordtvallem2  23573  txkgen  24015  cnmpt1st  24031  cnmpt2nd  24032  tmdgsum  24458  tsmssplit  24515  cnfldnm  25141  expcn  25237  pcorev2  25393  pi1xfrcnv  25422  rrxip  25755  mbfi1flim  26088  itg2uba  26108  itg2cnlem1  26126  itg2cnlem2  26127  itgitg2  26171  itgss3  26179  itgless  26181  ibladdlem  26184  itgaddlem1  26187  iblabslem  26192  itggt0  26208  itgcn  26209  limcdif  26240  limcres  26250  cnplimc  26251  dvcobr  26310  dvexp  26317  dveflem  26343  dvef  26344  dvlip  26357  dvlipcn  26358  lhop  26380  tdeglem2  26423  plyid  26571  coeidp  26626  dgrid  26627  plymulidp  26647  pserdvlem2  26801  abelth  26814  dvrelog  27011  logcn  27021  dvlog  27025  advlog  27028  advlogexp  27029  logtayl  27034  logccv  27037  dvcxp1  27114  dvsqrt  27116  dvcncxp1  27117  dvcnsqrt  27118  resqrtcn  27123  loglesqrt  27135  logblog  27166  dvatan  27309  leibpilem2  27315  leibpi  27316  efrlim  27343  sqrtlim  27346  amgmlem  27363  emcllem5  27373  lgamgulmlem2  27403  lgam1  27437  chtublem  27584  logfacrlim2  27599  bposlem6  27662  chto1lb  27851  vmadivsum  27855  dchrvmasumlema  27873  mulogsumlem  27904  logdivsum  27906  logsqvma2  27916  log2sumbnd  27917  selberglem1  27918  selberglem3  27920  selberg  27921  selberg2lem  27923  selberg2  27924  pntrmax  27937  pntrsumo1  27938  selbergr  27941  selbergs  27947  pnt2  27986  pnt  27987  ostth2  28010  ostth  28012  hilnormi  31811  bra0  32598  partfun2  33357  mplmonprod  34290  zrhre  34755  qqhre  34756  eulerpartgbij  35108  elmrsubrn  36486  faclim  36719  ptrest  38798  poimirlem19  38818  poimirlem20  38819  poimirlem30  38829  ovoliunnfl  38841  voliunnfl  38843  mbfposadd  38846  dvtan  38849  itg2addnclem  38850  ibladdnclem  38855  itgaddnclem1  38857  iblabsnclem  38862  itggt0cn  38869  ftc1anclem4  38875  ftc1anclem5  38876  ftc1anclem6  38877  ftc1anclem7  38878  ftc1anclem8  38879  dvasin  38883  dvacos  38884  areacirclem1  38887  dfadjliftmap2  39648  dfblockliftmap2  39652  aks6d1c1p5  43421  redvmptabs  43671  readvrec2  43672  readvrec  43673  readvcot  43675  arearect  44472  areaquad  44473  cantnfresb  44581  mptrcllem  44868  dfrcl2  44929  dfrcl3  44930  dftrcl3  44975  dfrtrcl3  44988  dfrtrcl4  44993  lhe4.4ex1a  45568  binomcxplemrat  45589  rnsnf  46466  feqresmptf  46510  limsupresre  46973  limsupvaluzmpt  46994  limsup10ex  47050  liminf10ex  47051  dvnprodlem1  47223  itgsin0pilem1  47227  wallispilem4  47345  wallispi2  47350  stirlinglem1  47351  stirlinglem3  47353  dirkercncflem2  47381  fourierdlem48  47431  fourierdlem49  47432  fourierdlem56  47439  fourierdlem57  47440  fourierdlem58  47441  fourierdlem62  47445  fourierdlem107  47490  fouriersw  47508  etransclem46  47557  sge0tsms  47657  sge0less  47669  sge0iun  47696  meadjun  47739  ovn02  47845  hoidmv1le  47871  hspmbllem2  47904  smflimsuplem3  48099  sqrtnpoly  48210  indprm  48981  indprmfz  48982  ackval1  50118  ackval2  50119  ackval3  50120  dftermo4  50962  dvsec  51278  dvcsc  51279  dvcot  51280