Theorem mpteq2ia 5252

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

Syntax hints:   → wi 4   = wceq 1540  ⊤wtru 1541   ∈ wcel 2105   ↦ cmpt 5232

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-opab 5212  df-mpt 5233

This theorem is referenced by:  mpteq2i  5254  partfun  6698  feqresmpt  6962  elfvmptrab  7027  fmptap  7171  offres  7973  resixpfo  8933  dfoi  9509  cantnflem1d  9686  cantnflem1  9687  dfceil2  13809  dfid5  14979  dfid6  14980  cnrecnv  15117  ackbijnn  15779  harmonic  15810  ege2le3  16038  eirrlem  16152  prmrec  16860  imasdsval2  17467  dfinito2  17958  dftermo2  17959  dfinito3  17960  dftermo3  17961  smndex1iidm  18819  smndex2dlinvh  18835  cayleylem1  19322  pmtrprfval  19397  gsumzsplit  19837  gsum2dlem2  19881  dmdprdsplitlem  19949  frlmip  21553  coe1sclmul  22025  coe1sclmul2  22027  mdetunilem9  22343  leordtvallem1  22935  leordtvallem2  22936  txkgen  23377  cnmpt1st  23393  cnmpt2nd  23394  tmdgsum  23820  tsmssplit  23877  cnfldnm  24516  expcn  24611  expcnOLD  24613  pcorev2  24776  pi1xfrcnv  24805  rrxip  25139  mbfi1flim  25474  itg2uba  25494  itg2cnlem1  25512  itg2cnlem2  25513  itgitg2  25557  itgss3  25565  itgless  25567  ibladdlem  25570  itgaddlem1  25573  iblabslem  25578  itggt0  25594  itgcn  25595  limcdif  25626  limcres  25636  cnplimc  25637  dvcobr  25696  dvexp  25703  dveflem  25729  dvef  25730  dvlip  25743  dvlipcn  25744  lhop  25766  tdeglem2  25812  plyid  25956  coeidp  26010  dgrid  26011  pserdvlem2  26173  abelth  26186  dvrelog  26378  logcn  26388  dvlog  26392  advlog  26395  advlogexp  26396  logtayl  26401  logccv  26404  dvcxp1  26481  dvsqrt  26483  dvcncxp1  26484  dvcnsqrt  26485  resqrtcn  26490  loglesqrt  26499  logblog  26530  dvatan  26673  leibpilem2  26679  leibpi  26680  efrlim  26707  sqrtlim  26710  amgmlem  26727  emcllem5  26737  lgamgulmlem2  26767  lgam1  26801  chtublem  26947  logfacrlim2  26962  bposlem6  27025  chto1lb  27214  vmadivsum  27218  dchrvmasumlema  27236  mulogsumlem  27267  logdivsum  27269  logsqvma2  27279  log2sumbnd  27280  selberglem1  27281  selberglem3  27283  selberg  27284  selberg2lem  27286  selberg2  27287  pntrmax  27300  pntrsumo1  27301  selbergr  27304  selbergs  27310  pnt2  27349  pnt  27350  ostth2  27373  ostth  27375  hilnormi  30680  bra0  31467  zrhre  33294  qqhre  33295  eulerpartgbij  33666  plymulx  33854  elmrsubrn  34806  faclim  35017  gg-dvcobr  35463  ptrest  36791  poimirlem19  36811  poimirlem20  36812  poimirlem30  36822  ovoliunnfl  36834  voliunnfl  36836  mbfposadd  36839  dvtan  36842  itg2addnclem  36843  ibladdnclem  36848  itgaddnclem1  36850  iblabsnclem  36855  itggt0cn  36862  ftc1anclem4  36868  ftc1anclem5  36869  ftc1anclem6  36870  ftc1anclem7  36871  ftc1anclem8  36872  dvasin  36876  dvacos  36877  areacirclem1  36880  arearect  42267  areaquad  42268  cantnfresb  42377  mptrcllem  42667  dfrcl2  42728  dfrcl3  42729  dftrcl3  42774  dfrtrcl3  42787  dfrtrcl4  42792  lhe4.4ex1a  43391  binomcxplemrat  43412  rnsnf  44183  feqresmptf  44231  limsupresre  44712  limsupvaluzmpt  44733  limsup10ex  44789  liminf10ex  44790  dvnprodlem1  44962  itgsin0pilem1  44966  wallispilem4  45084  wallispi2  45089  stirlinglem1  45090  stirlinglem3  45092  dirkercncflem2  45120  fourierdlem48  45170  fourierdlem49  45171  fourierdlem56  45178  fourierdlem57  45179  fourierdlem58  45180  fourierdlem62  45184  fourierdlem107  45229  fouriersw  45247  etransclem46  45296  sge0tsms  45396  sge0less  45408  sge0iun  45435  meadjun  45478  ovn02  45584  hoidmv1le  45610  hspmbllem2  45643  smflimsuplem3  45838  ackval1  47456  ackval2  47457  ackval3  47458