Theorem mpteq2ia 5202

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5170  df-mpt 5189

This theorem is referenced by:  mpteq2i  5203  partfun  6665  feqresmpt  6930  elfvmptrab  6997  fmptap  7144  offres  7962  resixpfo  8909  dfoi  9464  cantnflem1d  9641  cantnflem1  9642  dfceil2  13801  dfid5  14993  dfid6  14994  cnrecnv  15131  ackbijnn  15794  harmonic  15825  ege2le3  16056  eirrlem  16172  prmrec  16893  imasdsval2  17479  dfinito2  17965  dftermo2  17966  dfinito3  17967  dftermo3  17968  smndex1iidm  18828  smndex2dlinvh  18844  cayleylem1  19342  pmtrprfval  19417  gsumzsplit  19857  gsum2dlem2  19901  dmdprdsplitlem  19969  frlmip  21687  coe1sclmul  22168  coe1sclmul2  22170  mdetunilem9  22507  leordtvallem1  23097  leordtvallem2  23098  txkgen  23539  cnmpt1st  23555  cnmpt2nd  23556  tmdgsum  23982  tsmssplit  24039  cnfldnm  24666  expcn  24763  expcnOLD  24765  pcorev2  24928  pi1xfrcnv  24957  rrxip  25290  mbfi1flim  25624  itg2uba  25644  itg2cnlem1  25662  itg2cnlem2  25663  itgitg2  25708  itgss3  25716  itgless  25718  ibladdlem  25721  itgaddlem1  25724  iblabslem  25729  itggt0  25745  itgcn  25746  limcdif  25777  limcres  25787  cnplimc  25788  dvcobr  25849  dvcobrOLD  25850  dvexp  25857  dveflem  25883  dvef  25884  dvlip  25898  dvlipcn  25899  lhop  25921  tdeglem2  25966  plyid  26114  coeidp  26169  dgrid  26170  pserdvlem2  26338  abelth  26351  dvrelog  26546  logcn  26556  dvlog  26560  advlog  26563  advlogexp  26564  logtayl  26569  logccv  26572  dvcxp1  26649  dvsqrt  26651  dvcncxp1  26652  dvcnsqrt  26653  resqrtcn  26659  loglesqrt  26671  logblog  26702  dvatan  26845  leibpilem2  26851  leibpi  26852  efrlim  26879  efrlimOLD  26880  sqrtlim  26883  amgmlem  26900  emcllem5  26910  lgamgulmlem2  26940  lgam1  26974  chtublem  27122  logfacrlim2  27137  bposlem6  27200  chto1lb  27389  vmadivsum  27393  dchrvmasumlema  27411  mulogsumlem  27442  logdivsum  27444  logsqvma2  27454  log2sumbnd  27455  selberglem1  27456  selberglem3  27458  selberg  27459  selberg2lem  27461  selberg2  27462  pntrmax  27475  pntrsumo1  27476  selbergr  27479  selbergs  27485  pnt2  27524  pnt  27525  ostth2  27548  ostth  27550  hilnormi  31092  bra0  31879  zrhre  34009  qqhre  34010  eulerpartgbij  34363  plymulx  34539  elmrsubrn  35507  faclim  35733  ptrest  37613  poimirlem19  37633  poimirlem20  37634  poimirlem30  37644  ovoliunnfl  37656  voliunnfl  37658  mbfposadd  37661  dvtan  37664  itg2addnclem  37665  ibladdnclem  37670  itgaddnclem1  37672  iblabsnclem  37677  itggt0cn  37684  ftc1anclem4  37690  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  dvasin  37698  dvacos  37699  areacirclem1  37702  aks6d1c1p5  42100  redvmptabs  42348  readvrec2  42349  readvrec  42350  readvcot  42352  arearect  43204  areaquad  43205  cantnfresb  43313  mptrcllem  43602  dfrcl2  43663  dfrcl3  43664  dftrcl3  43709  dfrtrcl3  43722  dfrtrcl4  43727  lhe4.4ex1a  44318  binomcxplemrat  44339  rnsnf  45178  feqresmptf  45225  limsupresre  45694  limsupvaluzmpt  45715  limsup10ex  45771  liminf10ex  45772  dvnprodlem1  45944  itgsin0pilem1  45948  wallispilem4  46066  wallispi2  46071  stirlinglem1  46072  stirlinglem3  46074  dirkercncflem2  46102  fourierdlem48  46152  fourierdlem49  46153  fourierdlem56  46160  fourierdlem57  46161  fourierdlem58  46162  fourierdlem62  46166  fourierdlem107  46211  fouriersw  46229  etransclem46  46278  sge0tsms  46378  sge0less  46390  sge0iun  46417  meadjun  46460  ovn02  46566  hoidmv1le  46592  hspmbllem2  46625  smflimsuplem3  46820  ackval1  48670  ackval2  48671  ackval3  48672  dftermo4  49491