Theorem mpteq2ia 5221

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-opab 5187  df-mpt 5207

This theorem is referenced by:  mpteq2i  5222  partfun  6690  feqresmpt  6953  elfvmptrab  7020  fmptap  7167  offres  7987  resixpfo  8955  dfoi  9530  cantnflem1d  9707  cantnflem1  9708  dfceil2  13861  dfid5  15051  dfid6  15052  cnrecnv  15189  ackbijnn  15849  harmonic  15880  ege2le3  16111  eirrlem  16227  prmrec  16947  imasdsval2  17535  dfinito2  18021  dftermo2  18022  dfinito3  18023  dftermo3  18024  smndex1iidm  18884  smndex2dlinvh  18900  cayleylem1  19398  pmtrprfval  19473  gsumzsplit  19913  gsum2dlem2  19957  dmdprdsplitlem  20025  frlmip  21743  coe1sclmul  22224  coe1sclmul2  22226  mdetunilem9  22563  leordtvallem1  23153  leordtvallem2  23154  txkgen  23595  cnmpt1st  23611  cnmpt2nd  23612  tmdgsum  24038  tsmssplit  24095  cnfldnm  24722  expcn  24819  expcnOLD  24821  pcorev2  24984  pi1xfrcnv  25013  rrxip  25347  mbfi1flim  25681  itg2uba  25701  itg2cnlem1  25719  itg2cnlem2  25720  itgitg2  25765  itgss3  25773  itgless  25775  ibladdlem  25778  itgaddlem1  25781  iblabslem  25786  itggt0  25802  itgcn  25803  limcdif  25834  limcres  25844  cnplimc  25845  dvcobr  25906  dvcobrOLD  25907  dvexp  25914  dveflem  25940  dvef  25941  dvlip  25955  dvlipcn  25956  lhop  25978  tdeglem2  26023  plyid  26171  coeidp  26226  dgrid  26227  pserdvlem2  26395  abelth  26408  dvrelog  26603  logcn  26613  dvlog  26617  advlog  26620  advlogexp  26621  logtayl  26626  logccv  26629  dvcxp1  26706  dvsqrt  26708  dvcncxp1  26709  dvcnsqrt  26710  resqrtcn  26716  loglesqrt  26728  logblog  26759  dvatan  26902  leibpilem2  26908  leibpi  26909  efrlim  26936  efrlimOLD  26937  sqrtlim  26940  amgmlem  26957  emcllem5  26967  lgamgulmlem2  26997  lgam1  27031  chtublem  27179  logfacrlim2  27194  bposlem6  27257  chto1lb  27446  vmadivsum  27450  dchrvmasumlema  27468  mulogsumlem  27499  logdivsum  27501  logsqvma2  27511  log2sumbnd  27512  selberglem1  27513  selberglem3  27515  selberg  27516  selberg2lem  27518  selberg2  27519  pntrmax  27532  pntrsumo1  27533  selbergr  27536  selbergs  27542  pnt2  27581  pnt  27582  ostth2  27605  ostth  27607  hilnormi  31149  bra0  31936  zrhre  34055  qqhre  34056  eulerpartgbij  34409  plymulx  34585  elmrsubrn  35547  faclim  35768  ptrest  37648  poimirlem19  37668  poimirlem20  37669  poimirlem30  37679  ovoliunnfl  37691  voliunnfl  37693  mbfposadd  37696  dvtan  37699  itg2addnclem  37700  ibladdnclem  37705  itgaddnclem1  37707  iblabsnclem  37712  itggt0cn  37719  ftc1anclem4  37725  ftc1anclem5  37726  ftc1anclem6  37727  ftc1anclem7  37728  ftc1anclem8  37729  dvasin  37733  dvacos  37734  areacirclem1  37737  aks6d1c1p5  42130  redvmptabs  42378  readvrec2  42379  readvrec  42380  readvcot  42382  arearect  43214  areaquad  43215  cantnfresb  43323  mptrcllem  43612  dfrcl2  43673  dfrcl3  43674  dftrcl3  43719  dfrtrcl3  43732  dfrtrcl4  43737  lhe4.4ex1a  44328  binomcxplemrat  44349  rnsnf  45188  feqresmptf  45235  limsupresre  45705  limsupvaluzmpt  45726  limsup10ex  45782  liminf10ex  45783  dvnprodlem1  45955  itgsin0pilem1  45959  wallispilem4  46077  wallispi2  46082  stirlinglem1  46083  stirlinglem3  46085  dirkercncflem2  46113  fourierdlem48  46163  fourierdlem49  46164  fourierdlem56  46171  fourierdlem57  46172  fourierdlem58  46173  fourierdlem62  46177  fourierdlem107  46222  fouriersw  46240  etransclem46  46289  sge0tsms  46389  sge0less  46401  sge0iun  46428  meadjun  46471  ovn02  46577  hoidmv1le  46603  hspmbllem2  46636  smflimsuplem3  46831  ackval1  48641  ackval2  48642  ackval3  48643  dftermo4  49367