Theorem mpteq2ia 5251

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

Syntax hints:   → wi 4   = wceq 1537  ⊤wtru 1538   ∈ wcel 2106   ↦ cmpt 5231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-opab 5211  df-mpt 5232

This theorem is referenced by:  mpteq2i  5253  partfun  6716  feqresmpt  6978  elfvmptrab  7045  fmptap  7190  offres  8007  resixpfo  8975  dfoi  9549  cantnflem1d  9726  cantnflem1  9727  dfceil2  13876  dfid5  15063  dfid6  15064  cnrecnv  15201  ackbijnn  15861  harmonic  15892  ege2le3  16123  eirrlem  16237  prmrec  16956  imasdsval2  17563  dfinito2  18057  dftermo2  18058  dfinito3  18059  dftermo3  18060  smndex1iidm  18927  smndex2dlinvh  18943  cayleylem1  19445  pmtrprfval  19520  gsumzsplit  19960  gsum2dlem2  20004  dmdprdsplitlem  20072  frlmip  21816  coe1sclmul  22301  coe1sclmul2  22303  mdetunilem9  22642  leordtvallem1  23234  leordtvallem2  23235  txkgen  23676  cnmpt1st  23692  cnmpt2nd  23693  tmdgsum  24119  tsmssplit  24176  cnfldnm  24815  expcn  24910  expcnOLD  24912  pcorev2  25075  pi1xfrcnv  25104  rrxip  25438  mbfi1flim  25773  itg2uba  25793  itg2cnlem1  25811  itg2cnlem2  25812  itgitg2  25857  itgss3  25865  itgless  25867  ibladdlem  25870  itgaddlem1  25873  iblabslem  25878  itggt0  25894  itgcn  25895  limcdif  25926  limcres  25936  cnplimc  25937  dvcobr  25998  dvcobrOLD  25999  dvexp  26006  dveflem  26032  dvef  26033  dvlip  26047  dvlipcn  26048  lhop  26070  tdeglem2  26115  plyid  26263  coeidp  26318  dgrid  26319  pserdvlem2  26487  abelth  26500  dvrelog  26694  logcn  26704  dvlog  26708  advlog  26711  advlogexp  26712  logtayl  26717  logccv  26720  dvcxp1  26797  dvsqrt  26799  dvcncxp1  26800  dvcnsqrt  26801  resqrtcn  26807  loglesqrt  26819  logblog  26850  dvatan  26993  leibpilem2  26999  leibpi  27000  efrlim  27027  efrlimOLD  27028  sqrtlim  27031  amgmlem  27048  emcllem5  27058  lgamgulmlem2  27088  lgam1  27122  chtublem  27270  logfacrlim2  27285  bposlem6  27348  chto1lb  27537  vmadivsum  27541  dchrvmasumlema  27559  mulogsumlem  27590  logdivsum  27592  logsqvma2  27602  log2sumbnd  27603  selberglem1  27604  selberglem3  27606  selberg  27607  selberg2lem  27609  selberg2  27610  pntrmax  27623  pntrsumo1  27624  selbergr  27627  selbergs  27633  pnt2  27672  pnt  27673  ostth2  27696  ostth  27698  hilnormi  31192  bra0  31979  zrhre  33982  qqhre  33983  eulerpartgbij  34354  plymulx  34542  elmrsubrn  35505  faclim  35726  ptrest  37606  poimirlem19  37626  poimirlem20  37627  poimirlem30  37637  ovoliunnfl  37649  voliunnfl  37651  mbfposadd  37654  dvtan  37657  itg2addnclem  37658  ibladdnclem  37663  itgaddnclem1  37665  iblabsnclem  37670  itggt0cn  37677  ftc1anclem4  37683  ftc1anclem5  37684  ftc1anclem6  37685  ftc1anclem7  37686  ftc1anclem8  37687  dvasin  37691  dvacos  37692  areacirclem1  37695  aks6d1c1p5  42094  redvmptabs  42369  readvrec2  42370  readvrec  42371  arearect  43204  areaquad  43205  cantnfresb  43314  mptrcllem  43603  dfrcl2  43664  dfrcl3  43665  dftrcl3  43710  dfrtrcl3  43723  dfrtrcl4  43728  lhe4.4ex1a  44325  binomcxplemrat  44346  rnsnf  45127  feqresmptf  45174  limsupresre  45652  limsupvaluzmpt  45673  limsup10ex  45729  liminf10ex  45730  dvnprodlem1  45902  itgsin0pilem1  45906  wallispilem4  46024  wallispi2  46029  stirlinglem1  46030  stirlinglem3  46032  dirkercncflem2  46060  fourierdlem48  46110  fourierdlem49  46111  fourierdlem56  46118  fourierdlem57  46119  fourierdlem58  46120  fourierdlem62  46124  fourierdlem107  46169  fouriersw  46187  etransclem46  46236  sge0tsms  46336  sge0less  46348  sge0iun  46375  meadjun  46418  ovn02  46524  hoidmv1le  46550  hspmbllem2  46583  smflimsuplem3  46778  ackval1  48531  ackval2  48532  ackval3  48533