Theorem mpteq2ia 5192

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

Syntax hints:   → wi 4   = wceq 1559  ⊤wtru 1560   ∈ wcel 2141   ↦ cmpt 5178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5160  df-mpt 5179

This theorem is referenced by:  mpteq2i  5193  partfun  6663  feqresmpt  6931  elfvmptrab  7000  fmptap  7149  offres  7959  resixpfo  8912  dfoi  9453  cantnflem1d  9637  cantnflem1  9638  dfceil2  13843  dfid5  15034  dfid6  15035  cnrecnv  15183  ackbijnn  15849  harmonic  15880  ege2le3  16111  eirrlem  16227  prmrec  16949  imasdsval2  17537  dfinito2  18027  dftermo2  18028  dfinito3  18029  dftermo3  18030  smndex1iidm  18926  smndex2dlinvh  18945  cayleylem1  19443  pmtrprfval  19518  gsumzsplit  19958  gsum2dlem2  20002  dmdprdsplitlem  20070  frlmip  21818  coe1sclmul  22333  coe1sclmul2  22335  mdetunilem9  22668  leordtvallem1  23258  leordtvallem2  23259  txkgen  23700  cnmpt1st  23716  cnmpt2nd  23717  tmdgsum  24143  tsmssplit  24200  cnfldnm  24826  expcn  24922  pcorev2  25078  pi1xfrcnv  25107  rrxip  25440  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  25996  dvexp  26003  dveflem  26029  dvef  26030  dvlip  26043  dvlipcn  26044  lhop  26066  tdeglem2  26109  plyid  26257  coeidp  26311  dgrid  26312  plymulidp  26334  pserdvlem2  26479  abelth  26492  dvrelog  26690  logcn  26700  dvlog  26704  advlog  26707  advlogexp  26708  logtayl  26713  logccv  26716  dvcxp1  26793  dvsqrt  26795  dvcncxp1  26796  dvcnsqrt  26797  resqrtcn  26802  loglesqrt  26814  logblog  26845  dvatan  26988  leibpilem2  26994  leibpi  26995  efrlim  27022  sqrtlim  27025  amgmlem  27042  emcllem5  27052  lgamgulmlem2  27082  lgam1  27116  chtublem  27263  logfacrlim2  27278  bposlem6  27341  chto1lb  27530  vmadivsum  27534  dchrvmasumlema  27552  mulogsumlem  27583  logdivsum  27585  logsqvma2  27595  log2sumbnd  27596  selberglem1  27597  selberglem3  27599  selberg  27600  selberg2lem  27602  selberg2  27603  pntrmax  27616  pntrsumo1  27617  selbergr  27620  selbergs  27626  pnt2  27665  pnt  27666  ostth2  27689  ostth  27691  hilnormi  31323  bra0  32110  partfun2  32839  mplmonprod  33812  zrhre  34277  qqhre  34278  eulerpartgbij  34630  elmrsubrn  35831  faclim  36057  ptrest  38079  poimirlem19  38099  poimirlem20  38100  poimirlem30  38110  ovoliunnfl  38122  voliunnfl  38124  mbfposadd  38127  dvtan  38130  itg2addnclem  38131  ibladdnclem  38136  itgaddnclem1  38138  iblabsnclem  38143  itggt0cn  38150  ftc1anclem4  38156  ftc1anclem5  38157  ftc1anclem6  38158  ftc1anclem7  38159  ftc1anclem8  38160  dvasin  38164  dvacos  38165  areacirclem1  38168  dfadjliftmap2  38917  dfblockliftmap2  38921  aks6d1c1p5  42690  redvmptabs  42930  readvrec2  42931  readvrec  42932  readvcot  42934  arearect  43753  areaquad  43754  cantnfresb  43862  mptrcllem  44150  dfrcl2  44211  dfrcl3  44212  dftrcl3  44257  dfrtrcl3  44270  dfrtrcl4  44275  lhe4.4ex1a  44866  binomcxplemrat  44887  rnsnf  45723  feqresmptf  45767  limsupresre  46231  limsupvaluzmpt  46252  limsup10ex  46308  liminf10ex  46309  dvnprodlem1  46481  itgsin0pilem1  46485  wallispilem4  46603  wallispi2  46608  stirlinglem1  46609  stirlinglem3  46611  dirkercncflem2  46639  fourierdlem48  46689  fourierdlem49  46690  fourierdlem56  46697  fourierdlem57  46698  fourierdlem58  46699  fourierdlem62  46703  fourierdlem107  46748  fouriersw  46766  etransclem46  46815  sge0tsms  46915  sge0less  46927  sge0iun  46954  meadjun  46997  ovn02  47103  hoidmv1le  47129  hspmbllem2  47162  smflimsuplem3  47357  indprm  48199  indprmfz  48200  ackval1  49264  ackval2  49265  ackval3  49266  dftermo4  50084