Theorem mpteq2ia 5167

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

Syntax hints:   → wi 4   = wceq 1547  ⊤wtru 1548   ∈ wcel 2119   ↦ cmpt 5153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-opab 5135  df-mpt 5154

This theorem is referenced by:  mpteq2i  5168  partfun  6632  feqresmpt  6896  elfvmptrab  6965  fmptap  7114  offres  7925  resixpfo  8874  dfoi  9416  cantnflem1d  9600  cantnflem1  9601  dfceil2  13789  dfid5  14980  dfid6  14981  cnrecnv  15118  ackbijnn  15784  harmonic  15815  ege2le3  16046  eirrlem  16162  prmrec  16884  imasdsval2  17471  dfinito2  17961  dftermo2  17962  dfinito3  17963  dftermo3  17964  smndex1iidm  18860  smndex2dlinvh  18879  cayleylem1  19378  pmtrprfval  19453  gsumzsplit  19893  gsum2dlem2  19937  dmdprdsplitlem  20005  frlmip  21753  coe1sclmul  22268  coe1sclmul2  22270  mdetunilem9  22603  leordtvallem1  23193  leordtvallem2  23194  txkgen  23635  cnmpt1st  23651  cnmpt2nd  23652  tmdgsum  24078  tsmssplit  24135  cnfldnm  24761  expcn  24857  pcorev2  25013  pi1xfrcnv  25042  rrxip  25375  mbfi1flim  25708  itg2uba  25728  itg2cnlem1  25746  itg2cnlem2  25747  itgitg2  25792  itgss3  25800  itgless  25802  ibladdlem  25805  itgaddlem1  25808  iblabslem  25813  itggt0  25829  itgcn  25830  limcdif  25861  limcres  25871  cnplimc  25872  dvcobr  25931  dvexp  25938  dveflem  25964  dvef  25965  dvlip  25978  dvlipcn  25979  lhop  26001  tdeglem2  26044  plyid  26192  coeidp  26246  dgrid  26247  pserdvlem2  26411  abelth  26424  dvrelog  26619  logcn  26629  dvlog  26633  advlog  26636  advlogexp  26637  logtayl  26642  logccv  26645  dvcxp1  26722  dvsqrt  26724  dvcncxp1  26725  dvcnsqrt  26726  resqrtcn  26731  loglesqrt  26743  logblog  26774  dvatan  26917  leibpilem2  26923  leibpi  26924  efrlim  26951  sqrtlim  26954  amgmlem  26971  emcllem5  26981  lgamgulmlem2  27011  lgam1  27045  chtublem  27192  logfacrlim2  27207  bposlem6  27270  chto1lb  27459  vmadivsum  27463  dchrvmasumlema  27481  mulogsumlem  27512  logdivsum  27514  logsqvma2  27524  log2sumbnd  27525  selberglem1  27526  selberglem3  27528  selberg  27529  selberg2lem  27531  selberg2  27532  pntrmax  27545  pntrsumo1  27546  selbergr  27549  selbergs  27555  pnt2  27594  pnt  27595  ostth2  27618  ostth  27620  hilnormi  31252  bra0  32039  partfun2  32768  mplmonprod  33738  zrhre  34203  qqhre  34204  eulerpartgbij  34556  plymulx  34732  elmrsubrn  35748  faclim  35974  ptrest  37986  poimirlem19  38006  poimirlem20  38007  poimirlem30  38017  ovoliunnfl  38029  voliunnfl  38031  mbfposadd  38034  dvtan  38037  itg2addnclem  38038  ibladdnclem  38043  itgaddnclem1  38045  iblabsnclem  38050  itggt0cn  38057  ftc1anclem4  38063  ftc1anclem5  38064  ftc1anclem6  38065  ftc1anclem7  38066  ftc1anclem8  38067  dvasin  38071  dvacos  38072  areacirclem1  38075  dfadjliftmap2  38824  dfblockliftmap2  38828  aks6d1c1p5  42597  redvmptabs  42837  readvrec2  42838  readvrec  42839  readvcot  42841  arearect  43660  areaquad  43661  cantnfresb  43769  mptrcllem  44057  dfrcl2  44118  dfrcl3  44119  dftrcl3  44164  dfrtrcl3  44177  dfrtrcl4  44182  lhe4.4ex1a  44773  binomcxplemrat  44794  rnsnf  45631  feqresmptf  45675  limsupresre  46139  limsupvaluzmpt  46160  limsup10ex  46216  liminf10ex  46217  dvnprodlem1  46389  itgsin0pilem1  46393  wallispilem4  46511  wallispi2  46516  stirlinglem1  46517  stirlinglem3  46519  dirkercncflem2  46547  fourierdlem48  46597  fourierdlem49  46598  fourierdlem56  46605  fourierdlem57  46606  fourierdlem58  46607  fourierdlem62  46611  fourierdlem107  46656  fouriersw  46674  etransclem46  46723  sge0tsms  46823  sge0less  46835  sge0iun  46862  meadjun  46905  ovn02  47011  hoidmv1le  47037  hspmbllem2  47070  smflimsuplem3  47265  indprm  48107  indprmfz  48108  ackval1  49172  ackval2  49173  ackval3  49174  dftermo4  49992