Theorem mpteq2ia 5177

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

Syntax hints:   → wi 4   = wceq 1539  ⊤wtru 1540   ∈ wcel 2106   ↦ cmpt 5157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-opab 5137  df-mpt 5158

This theorem is referenced by:  mpteq2i  5179  partfun  6580  feqresmpt  6838  elfvmptrab  6903  fmptap  7042  offres  7826  resixpfo  8724  dfoi  9270  cantnflem1d  9446  cantnflem1  9447  dfceil2  13559  dfid5  14738  dfid6  14739  cnrecnv  14876  ackbijnn  15540  harmonic  15571  ege2le3  15799  eirrlem  15913  prmrec  16623  imasdsval2  17227  dfinito2  17718  dftermo2  17719  dfinito3  17720  dftermo3  17721  smndex1iidm  18540  smndex2dlinvh  18556  cayleylem1  19020  pmtrprfval  19095  gsumzsplit  19528  gsum2dlem2  19572  dmdprdsplitlem  19640  frlmip  20985  coe1sclmul  21453  coe1sclmul2  21455  mdetunilem9  21769  leordtvallem1  22361  leordtvallem2  22362  txkgen  22803  cnmpt1st  22819  cnmpt2nd  22820  tmdgsum  23246  tsmssplit  23303  cnfldnm  23942  expcn  24035  pcorev2  24191  pi1xfrcnv  24220  rrxip  24554  mbfi1flim  24888  itg2uba  24908  itg2cnlem1  24926  itg2cnlem2  24927  itgitg2  24971  itgss3  24979  itgless  24981  ibladdlem  24984  itgaddlem1  24987  iblabslem  24992  itggt0  25008  itgcn  25009  limcdif  25040  limcres  25050  cnplimc  25051  dvcobr  25110  dvexp  25117  dveflem  25143  dvef  25144  dvlip  25157  dvlipcn  25158  lhop  25180  tdeglem2  25226  plyid  25370  coeidp  25424  dgrid  25425  pserdvlem2  25587  abelth  25600  dvrelog  25792  logcn  25802  dvlog  25806  advlog  25809  advlogexp  25810  logtayl  25815  logccv  25818  dvcxp1  25893  dvsqrt  25895  dvcncxp1  25896  dvcnsqrt  25897  resqrtcn  25902  loglesqrt  25911  logblog  25942  dvatan  26085  leibpilem2  26091  leibpi  26092  efrlim  26119  sqrtlim  26122  amgmlem  26139  emcllem5  26149  lgamgulmlem2  26179  lgam1  26213  chtublem  26359  logfacrlim2  26374  bposlem6  26437  chto1lb  26626  vmadivsum  26630  dchrvmasumlema  26648  mulogsumlem  26679  logdivsum  26681  logsqvma2  26691  log2sumbnd  26692  selberglem1  26693  selberglem3  26695  selberg  26696  selberg2lem  26698  selberg2  26699  pntrmax  26712  pntrsumo1  26713  selbergr  26716  selbergs  26722  pnt2  26761  pnt  26762  ostth2  26785  ostth  26787  hilnormi  29525  bra0  30312  zrhre  31969  qqhre  31970  eulerpartgbij  32339  plymulx  32527  elmrsubrn  33482  faclim  33712  ptrest  35776  poimirlem19  35796  poimirlem20  35797  poimirlem30  35807  ovoliunnfl  35819  voliunnfl  35821  mbfposadd  35824  dvtan  35827  itg2addnclem  35828  ibladdnclem  35833  itgaddnclem1  35835  iblabsnclem  35840  itggt0cn  35847  ftc1anclem4  35853  ftc1anclem5  35854  ftc1anclem6  35855  ftc1anclem7  35856  ftc1anclem8  35857  dvasin  35861  dvacos  35862  areacirclem1  35865  arearect  41046  areaquad  41047  mptrcllem  41221  dfrcl2  41282  dfrcl3  41283  dftrcl3  41328  dfrtrcl3  41341  dfrtrcl4  41346  lhe4.4ex1a  41947  binomcxplemrat  41968  rnsnf  42721  feqresmptf  42772  limsupresre  43237  limsupvaluzmpt  43258  limsup10ex  43314  liminf10ex  43315  dvnprodlem1  43487  itgsin0pilem1  43491  wallispilem4  43609  wallispi2  43614  stirlinglem1  43615  stirlinglem3  43617  dirkercncflem2  43645  fourierdlem48  43695  fourierdlem49  43696  fourierdlem56  43703  fourierdlem57  43704  fourierdlem58  43705  fourierdlem62  43709  fourierdlem107  43754  fouriersw  43772  etransclem46  43821  sge0tsms  43918  sge0less  43930  sge0iun  43957  meadjun  44000  ovn02  44106  hoidmv1le  44132  hspmbllem2  44165  smflimsuplem3  44355  ackval1  46027  ackval2  46028  ackval3  46029