Theorem mpteq2ia 4668

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 2610	. . 3 ⊢ 𝐴 = 𝐴
2	1	ax-gen 1713	. 2 ⊢ ∀𝑥 𝐴 = 𝐴
3		mpteq2ia.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)
4	3	rgen 2906	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶
5		mpteq12f 4661	. 2 ⊢ ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
6	2, 4, 5	mp2an 704	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4  ∀wal 1473   = wceq 1475   ∈ wcel 1977  ∀wral 2896   ↦ cmpt 4643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ral 2901  df-opab 4644  df-mpt 4645

This theorem is referenced by:  mpteq2i  4669  feqresmpt  6160  elfvmptrab  6214  fmptap  6341  offres  7054  resixpfo  7832  dfoi  8299  cantnflem1d  8468  cantnflem1  8469  dfceil2  12502  dfid5  13615  dfid6  13616  cnrecnv  13753  ackbijnn  14399  harmonic  14430  ege2le3  14659  eirrlem  14771  prmrec  15464  imasdsval2  15999  cayleylem1  17655  pmtrprfval  17730  gsumzsplit  18150  gsum2dlem2  18193  dmdprdsplitlem  18259  coe1sclmul  19473  coe1sclmul2  19475  frlmip  19936  mdetunilem9  20245  leordtvallem1  20824  leordtvallem2  20825  txkgen  21265  cnmpt1st  21281  cnmpt2nd  21282  tmdgsum  21709  tsmssplit  21765  cnfldnm  22392  expcn  22483  pcorev2  22636  pi1xfrcnv  22665  rrxip  22986  mbfi1flim  23296  itg2uba  23316  itg2cnlem1  23334  itg2cnlem2  23335  itgitg2  23379  itgss3  23387  itgless  23389  ibladdlem  23392  itgaddlem1  23395  iblabslem  23400  itggt0  23414  itgcn  23415  limcdif  23446  limcres  23456  cnplimc  23457  dvcobr  23515  dvexp  23522  dveflem  23546  dvef  23547  dvlip  23560  dvlipcn  23561  lhop  23583  tdeglem2  23625  plyid  23769  coeidp  23823  dgrid  23824  pserdvlem2  23986  abelth  23999  dvrelog  24183  logcn  24193  dvlog  24197  advlog  24200  advlogexp  24201  logtayl  24206  logccv  24209  dvcxp1  24281  dvsqrt  24283  dvcncxp1  24284  dvcnsqrt  24285  resqrtcn  24290  loglesqrt  24299  logblog  24330  dvatan  24462  leibpilem2  24468  leibpi  24469  efrlim  24496  sqrtlim  24499  amgmlem  24516  emcllem5  24526  lgamgulmlem2  24556  lgam1  24590  chtublem  24736  logfacrlim2  24751  bposlem6  24814  chto1lb  24967  vmadivsum  24971  dchrvmasumlema  24989  mulogsumlem  25020  logdivsum  25022  logsqvma2  25032  log2sumbnd  25033  selberglem1  25034  selberglem3  25036  selberg  25037  selberg2lem  25039  selberg2  25040  pntrmax  25053  pntrsumo1  25054  selbergr  25057  selbergs  25063  pnt2  25102  pnt  25103  ostth2  25126  ostth  25128  hilnormi  27404  bra0  28193  partfun  28858  zrhre  29391  qqhre  29392  eulerpartgbij  29761  plymulx  29951  faclim  30885  ptrest  32578  poimirlem19  32598  poimirlem20  32599  poimirlem30  32609  ovoliunnfl  32621  voliunnfl  32623  mbfposadd  32627  dvtan  32630  itg2addnclem  32631  ibladdnclem  32636  itgaddnclem1  32638  iblabsnclem  32643  itggt0cn  32652  ftc1anclem4  32658  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  dvasin  32666  dvacos  32667  areacirclem1  32670  arearect  36820  areaquad  36821  mptrcllem  36939  dfrcl2  36985  dfrcl3  36986  dftrcl3  37031  dfrtrcl3  37044  dfrtrcl4  37049  lhe4.4ex1a  37550  binomcxplemrat  37571  rnsnf  38365  dvnprodlem1  38836  itgsin0pilem1  38841  wallispilem4  38961  wallispi2  38966  stirlinglem1  38967  stirlinglem3  38969  dirkercncflem2  38997  fourierdlem48  39047  fourierdlem49  39048  fourierdlem56  39055  fourierdlem57  39056  fourierdlem58  39057  fourierdlem62  39061  fourierdlem107  39106  fouriersw  39124  etransclem46  39173  sge0tsms  39273  sge0less  39285  sge0iun  39312  meadjun  39355  ovn02  39458  hoidmv1le  39484  hspmbllem2  39517