Theorem mpteq2ia 5121

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)

Hypothesis

Ref	Expression
mpteq2ia.1	⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)

Assertion

Ref	Expression
mpteq2ia	⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Proof of Theorem mpteq2ia

Step	Hyp	Ref	Expression
1		eqid 2798	. . 3 ⊢ 𝐴 = 𝐴
2	1	ax-gen 1797	. 2 ⊢ ∀𝑥 𝐴 = 𝐴
3		mpteq2ia.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)
4	3	rgen 3116	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶
5		mpteq12f 5113	. 2 ⊢ ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
6	2, 4, 5	mp2an 691	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4  ∀wal 1536   = wceq 1538   ∈ wcel 2111  ∀wral 3106   ↦ cmpt 5110

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-opab 5093  df-mpt 5111

This theorem is referenced by:  mpteq2i  5122  partfun  6467  feqresmpt  6709  elfvmptrab  6773  fmptap  6909  offres  7666  resixpfo  8483  dfoi  8959  cantnflem1d  9135  cantnflem1  9136  dfceil2  13204  dfid5  14378  dfid6  14379  cnrecnv  14516  ackbijnn  15175  harmonic  15206  ege2le3  15435  eirrlem  15549  prmrec  16248  imasdsval2  16781  smndex1iidm  18058  smndex2dlinvh  18074  cayleylem1  18532  pmtrprfval  18607  gsumzsplit  19040  gsum2dlem2  19084  dmdprdsplitlem  19152  frlmip  20467  coe1sclmul  20911  coe1sclmul2  20913  mdetunilem9  21225  leordtvallem1  21815  leordtvallem2  21816  txkgen  22257  cnmpt1st  22273  cnmpt2nd  22274  tmdgsum  22700  tsmssplit  22757  cnfldnm  23384  expcn  23477  pcorev2  23633  pi1xfrcnv  23662  rrxip  23994  mbfi1flim  24327  itg2uba  24347  itg2cnlem1  24365  itg2cnlem2  24366  itgitg2  24410  itgss3  24418  itgless  24420  ibladdlem  24423  itgaddlem1  24426  iblabslem  24431  itggt0  24447  itgcn  24448  limcdif  24479  limcres  24489  cnplimc  24490  dvcobr  24549  dvexp  24556  dveflem  24582  dvef  24583  dvlip  24596  dvlipcn  24597  lhop  24619  tdeglem2  24662  plyid  24806  coeidp  24860  dgrid  24861  pserdvlem2  25023  abelth  25036  dvrelog  25228  logcn  25238  dvlog  25242  advlog  25245  advlogexp  25246  logtayl  25251  logccv  25254  dvcxp1  25329  dvsqrt  25331  dvcncxp1  25332  dvcnsqrt  25333  resqrtcn  25338  loglesqrt  25347  logblog  25378  dvatan  25521  leibpilem2  25527  leibpi  25528  efrlim  25555  sqrtlim  25558  amgmlem  25575  emcllem5  25585  lgamgulmlem2  25615  lgam1  25649  chtublem  25795  logfacrlim2  25810  bposlem6  25873  chto1lb  26062  vmadivsum  26066  dchrvmasumlema  26084  mulogsumlem  26115  logdivsum  26117  logsqvma2  26127  log2sumbnd  26128  selberglem1  26129  selberglem3  26131  selberg  26132  selberg2lem  26134  selberg2  26135  pntrmax  26148  pntrsumo1  26149  selbergr  26152  selbergs  26158  pnt2  26197  pnt  26198  ostth2  26221  ostth  26223  hilnormi  28946  bra0  29733  zrhre  31370  qqhre  31371  eulerpartgbij  31740  plymulx  31928  elmrsubrn  32880  faclim  33091  ptrest  35056  poimirlem19  35076  poimirlem20  35077  poimirlem30  35087  ovoliunnfl  35099  voliunnfl  35101  mbfposadd  35104  dvtan  35107  itg2addnclem  35108  ibladdnclem  35113  itgaddnclem1  35115  iblabsnclem  35120  itggt0cn  35127  ftc1anclem4  35133  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anclem8  35137  dvasin  35141  dvacos  35142  areacirclem1  35145  arearect  40165  areaquad  40166  mptrcllem  40313  dfrcl2  40375  dfrcl3  40376  dftrcl3  40421  dfrtrcl3  40434  dfrtrcl4  40439  lhe4.4ex1a  41033  binomcxplemrat  41054  rnsnf  41810  feqresmptf  41865  limsupresre  42338  limsupvaluzmpt  42359  limsup10ex  42415  liminf10ex  42416  dvnprodlem1  42588  itgsin0pilem1  42592  wallispilem4  42710  wallispi2  42715  stirlinglem1  42716  stirlinglem3  42718  dirkercncflem2  42746  fourierdlem48  42796  fourierdlem49  42797  fourierdlem56  42804  fourierdlem57  42805  fourierdlem58  42806  fourierdlem62  42810  fourierdlem107  42855  fouriersw  42873  etransclem46  42922  sge0tsms  43019  sge0less  43031  sge0iun  43058  meadjun  43101  ovn02  43207  hoidmv1le  43233  hspmbllem2  43266  smflimsuplem3  43453  ackval1  45095  ackval2  45096  ackval3  45097