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 1549	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5149  df-mpt 5168

This theorem is referenced by:  mpteq2i  5182  partfun  6639  feqresmpt  6903  elfvmptrab  6971  fmptap  7118  offres  7929  resixpfo  8877  dfoi  9419  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  21768  coe1sclmul  22257  coe1sclmul2  22259  mdetunilem9  22595  leordtvallem1  23185  leordtvallem2  23186  txkgen  23627  cnmpt1st  23643  cnmpt2nd  23644  tmdgsum  24070  tsmssplit  24127  cnfldnm  24753  expcn  24849  pcorev2  25005  pi1xfrcnv  25034  rrxip  25367  mbfi1flim  25700  itg2uba  25720  itg2cnlem1  25738  itg2cnlem2  25739  itgitg2  25784  itgss3  25792  itgless  25794  ibladdlem  25797  itgaddlem1  25800  iblabslem  25805  itggt0  25821  itgcn  25822  limcdif  25853  limcres  25863  cnplimc  25864  dvcobr  25923  dvexp  25930  dveflem  25956  dvef  25957  dvlip  25970  dvlipcn  25971  lhop  25993  tdeglem2  26036  plyid  26184  coeidp  26238  dgrid  26239  pserdvlem2  26406  abelth  26419  dvrelog  26614  logcn  26624  dvlog  26628  advlog  26631  advlogexp  26632  logtayl  26637  logccv  26640  dvcxp1  26717  dvsqrt  26719  dvcncxp1  26720  dvcnsqrt  26721  resqrtcn  26726  loglesqrt  26738  logblog  26769  dvatan  26912  leibpilem2  26918  leibpi  26919  efrlim  26946  efrlimOLD  26947  sqrtlim  26950  amgmlem  26967  emcllem5  26977  lgamgulmlem2  27007  lgam1  27041  chtublem  27188  logfacrlim2  27203  bposlem6  27266  chto1lb  27455  vmadivsum  27459  dchrvmasumlema  27477  mulogsumlem  27508  logdivsum  27510  logsqvma2  27520  log2sumbnd  27521  selberglem1  27522  selberglem3  27524  selberg  27525  selberg2lem  27527  selberg2  27528  pntrmax  27541  pntrsumo1  27542  selbergr  27545  selbergs  27551  pnt2  27590  pnt  27591  ostth2  27614  ostth  27616  hilnormi  31249  bra0  32036  partfun2  32764  mplmonprod  33713  zrhre  34179  qqhre  34180  eulerpartgbij  34532  plymulx  34708  elmrsubrn  35718  faclim  35944  ptrest  37954  poimirlem19  37974  poimirlem20  37975  poimirlem30  37985  ovoliunnfl  37997  voliunnfl  37999  mbfposadd  38002  dvtan  38005  itg2addnclem  38006  ibladdnclem  38011  itgaddnclem1  38013  iblabsnclem  38018  itggt0cn  38025  ftc1anclem4  38031  ftc1anclem5  38032  ftc1anclem6  38033  ftc1anclem7  38034  ftc1anclem8  38035  dvasin  38039  dvacos  38040  areacirclem1  38043  dfadjliftmap2  38792  dfblockliftmap2  38796  aks6d1c1p5  42565  redvmptabs  42806  readvrec2  42807  readvrec  42808  readvcot  42810  arearect  43661  areaquad  43662  cantnfresb  43770  mptrcllem  44058  dfrcl2  44119  dfrcl3  44120  dftrcl3  44165  dfrtrcl3  44178  dfrtrcl4  44183  lhe4.4ex1a  44774  binomcxplemrat  44795  rnsnf  45632  feqresmptf  45678  limsupresre  46142  limsupvaluzmpt  46163  limsup10ex  46219  liminf10ex  46220  dvnprodlem1  46392  itgsin0pilem1  46396  wallispilem4  46514  wallispi2  46519  stirlinglem1  46520  stirlinglem3  46522  dirkercncflem2  46550  fourierdlem48  46600  fourierdlem49  46601  fourierdlem56  46608  fourierdlem57  46609  fourierdlem58  46610  fourierdlem62  46614  fourierdlem107  46659  fouriersw  46677  etransclem46  46726  sge0tsms  46826  sge0less  46838  sge0iun  46865  meadjun  46908  ovn02  47014  hoidmv1le  47040  hspmbllem2  47073  smflimsuplem3  47268  indprm  48104  indprmfz  48105  ackval1  49169  ackval2  49170  ackval3  49171  dftermo4  49989