Theorem mpteq2ia 5206

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

Syntax hints:   → wi 4   = wceq 1570  ⊤wtru 1571   ∈ wcel 2143   ↦ cmpt 5192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5174  df-mpt 5193

This theorem is referenced by:  mpteq2i  5207  partfun  6682  feqresmpt  6950  elfvmptrab  7019  fmptap  7168  offres  7976  resixpfo  8930  dfoi  9469  cantnflem1d  9653  cantnflem1  9654  dfceil2  13868  dfid5  15060  dfid6  15061  cnrecnv  15212  ackbijnn  15878  harmonic  15909  ege2le3  16139  eirrlem  16255  prmrec  16977  imasdsval2  17565  dfinito2  18055  dftermo2  18056  dfinito3  18057  dftermo3  18058  smndex1iidm  18955  smndex2dlinvh  18974  cayleylem1  19477  pmtrprfval  19552  gsumzsplit  19992  gsum2dlem2  20036  dmdprdsplitlem  20104  frlmip  21928  coe1sclmul  22443  coe1sclmul2  22445  mdetunilem9  22777  leordtvallem1  23367  leordtvallem2  23368  txkgen  23809  cnmpt1st  23825  cnmpt2nd  23826  tmdgsum  24252  tsmssplit  24309  cnfldnm  24935  expcn  25031  pcorev2  25187  pi1xfrcnv  25216  rrxip  25549  mbfi1flim  25882  itg2uba  25902  itg2cnlem1  25920  itg2cnlem2  25921  itgitg2  25966  itgss3  25974  itgless  25976  ibladdlem  25979  itgaddlem1  25982  iblabslem  25987  itggt0  26003  itgcn  26004  limcdif  26035  limcres  26045  cnplimc  26046  dvcobr  26105  dvexp  26112  dveflem  26138  dvef  26139  dvlip  26152  dvlipcn  26153  lhop  26175  tdeglem2  26218  plyid  26366  coeidp  26420  dgrid  26421  plymulidp  26443  pserdvlem2  26591  abelth  26604  dvrelog  26802  logcn  26812  dvlog  26816  advlog  26819  advlogexp  26820  logtayl  26825  logccv  26828  dvcxp1  26905  dvsqrt  26907  dvcncxp1  26908  dvcnsqrt  26909  resqrtcn  26914  loglesqrt  26926  logblog  26957  dvatan  27100  leibpilem2  27106  leibpi  27107  efrlim  27134  sqrtlim  27137  amgmlem  27154  emcllem5  27164  lgamgulmlem2  27194  lgam1  27228  chtublem  27375  logfacrlim2  27390  bposlem6  27453  chto1lb  27642  vmadivsum  27646  dchrvmasumlema  27664  mulogsumlem  27695  logdivsum  27697  logsqvma2  27707  log2sumbnd  27708  selberglem1  27709  selberglem3  27711  selberg  27712  selberg2lem  27714  selberg2  27715  pntrmax  27728  pntrsumo1  27729  selbergr  27732  selbergs  27738  pnt2  27777  pnt  27778  ostth2  27801  ostth  27803  hilnormi  31515  bra0  32302  partfun2  33021  mplmonprod  33944  zrhre  34409  qqhre  34410  eulerpartgbij  34762  elmrsubrn  36012  faclim  36238  ptrest  38270  poimirlem19  38290  poimirlem20  38291  poimirlem30  38301  ovoliunnfl  38313  voliunnfl  38315  mbfposadd  38318  dvtan  38321  itg2addnclem  38322  ibladdnclem  38327  itgaddnclem1  38329  iblabsnclem  38334  itggt0cn  38341  ftc1anclem4  38347  ftc1anclem5  38348  ftc1anclem6  38349  ftc1anclem7  38350  ftc1anclem8  38351  dvasin  38355  dvacos  38356  areacirclem1  38359  dfadjliftmap2  39106  dfblockliftmap2  39110  aks6d1c1p5  42879  redvmptabs  43121  readvrec2  43122  readvrec  43123  readvcot  43125  arearect  43942  areaquad  43943  cantnfresb  44051  mptrcllem  44339  dfrcl2  44400  dfrcl3  44401  dftrcl3  44446  dfrtrcl3  44459  dfrtrcl4  44464  lhe4.4ex1a  45039  binomcxplemrat  45060  rnsnf  45902  feqresmptf  45946  limsupresre  46410  limsupvaluzmpt  46431  limsup10ex  46487  liminf10ex  46488  dvnprodlem1  46660  itgsin0pilem1  46664  wallispilem4  46782  wallispi2  46787  stirlinglem1  46788  stirlinglem3  46790  dirkercncflem2  46818  fourierdlem48  46868  fourierdlem49  46869  fourierdlem56  46876  fourierdlem57  46877  fourierdlem58  46878  fourierdlem62  46882  fourierdlem107  46927  fouriersw  46945  etransclem46  46994  sge0tsms  47094  sge0less  47106  sge0iun  47133  meadjun  47176  ovn02  47282  hoidmv1le  47308  hspmbllem2  47341  smflimsuplem3  47536  indprm  48381  indprmfz  48382  ackval1  49461  ackval2  49462  ackval3  49463  dftermo4  50280