Theorem mpteq2ia 5181

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

Syntax hints:   → wi 4   = wceq 1541  ⊤wtru 1542   ∈ wcel 2111   ↦ cmpt 5167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-opab 5149  df-mpt 5168

This theorem is referenced by:  mpteq2i  5182  partfun  6623  feqresmpt  6886  elfvmptrab  6953  fmptap  7099  offres  7910  resixpfo  8855  dfoi  9392  cantnflem1d  9573  cantnflem1  9574  dfceil2  13738  dfid5  14929  dfid6  14930  cnrecnv  15067  ackbijnn  15730  harmonic  15761  ege2le3  15992  eirrlem  16108  prmrec  16829  imasdsval2  17415  dfinito2  17905  dftermo2  17906  dfinito3  17907  dftermo3  17908  smndex1iidm  18804  smndex2dlinvh  18820  cayleylem1  19319  pmtrprfval  19394  gsumzsplit  19834  gsum2dlem2  19878  dmdprdsplitlem  19946  frlmip  21710  coe1sclmul  22191  coe1sclmul2  22193  mdetunilem9  22530  leordtvallem1  23120  leordtvallem2  23121  txkgen  23562  cnmpt1st  23578  cnmpt2nd  23579  tmdgsum  24005  tsmssplit  24062  cnfldnm  24688  expcn  24785  expcnOLD  24787  pcorev2  24950  pi1xfrcnv  24979  rrxip  25312  mbfi1flim  25646  itg2uba  25666  itg2cnlem1  25684  itg2cnlem2  25685  itgitg2  25730  itgss3  25738  itgless  25740  ibladdlem  25743  itgaddlem1  25746  iblabslem  25751  itggt0  25767  itgcn  25768  limcdif  25799  limcres  25809  cnplimc  25810  dvcobr  25871  dvcobrOLD  25872  dvexp  25879  dveflem  25905  dvef  25906  dvlip  25920  dvlipcn  25921  lhop  25943  tdeglem2  25988  plyid  26136  coeidp  26191  dgrid  26192  pserdvlem2  26360  abelth  26373  dvrelog  26568  logcn  26578  dvlog  26582  advlog  26585  advlogexp  26586  logtayl  26591  logccv  26594  dvcxp1  26671  dvsqrt  26673  dvcncxp1  26674  dvcnsqrt  26675  resqrtcn  26681  loglesqrt  26693  logblog  26724  dvatan  26867  leibpilem2  26873  leibpi  26874  efrlim  26901  efrlimOLD  26902  sqrtlim  26905  amgmlem  26922  emcllem5  26932  lgamgulmlem2  26962  lgam1  26996  chtublem  27144  logfacrlim2  27159  bposlem6  27222  chto1lb  27411  vmadivsum  27415  dchrvmasumlema  27433  mulogsumlem  27464  logdivsum  27466  logsqvma2  27476  log2sumbnd  27477  selberglem1  27478  selberglem3  27480  selberg  27481  selberg2lem  27483  selberg2  27484  pntrmax  27497  pntrsumo1  27498  selbergr  27501  selbergs  27507  pnt2  27546  pnt  27547  ostth2  27570  ostth  27572  hilnormi  31135  bra0  31922  zrhre  34024  qqhre  34025  eulerpartgbij  34377  plymulx  34553  elmrsubrn  35556  faclim  35782  ptrest  37659  poimirlem19  37679  poimirlem20  37680  poimirlem30  37690  ovoliunnfl  37702  voliunnfl  37704  mbfposadd  37707  dvtan  37710  itg2addnclem  37711  ibladdnclem  37716  itgaddnclem1  37718  iblabsnclem  37723  itggt0cn  37730  ftc1anclem4  37736  ftc1anclem5  37737  ftc1anclem6  37738  ftc1anclem7  37739  ftc1anclem8  37740  dvasin  37744  dvacos  37745  areacirclem1  37748  aks6d1c1p5  42145  redvmptabs  42393  readvrec2  42394  readvrec  42395  readvcot  42397  arearect  43248  areaquad  43249  cantnfresb  43357  mptrcllem  43646  dfrcl2  43707  dfrcl3  43708  dftrcl3  43753  dfrtrcl3  43766  dfrtrcl4  43771  lhe4.4ex1a  44362  binomcxplemrat  44383  rnsnf  45221  feqresmptf  45268  limsupresre  45734  limsupvaluzmpt  45755  limsup10ex  45811  liminf10ex  45812  dvnprodlem1  45984  itgsin0pilem1  45988  wallispilem4  46106  wallispi2  46111  stirlinglem1  46112  stirlinglem3  46114  dirkercncflem2  46142  fourierdlem48  46192  fourierdlem49  46193  fourierdlem56  46200  fourierdlem57  46201  fourierdlem58  46202  fourierdlem62  46206  fourierdlem107  46251  fouriersw  46269  etransclem46  46318  sge0tsms  46418  sge0less  46430  sge0iun  46457  meadjun  46500  ovn02  46606  hoidmv1le  46632  hspmbllem2  46665  smflimsuplem3  46860  ackval1  48713  ackval2  48714  ackval3  48715  dftermo4  49534