Theorem mpteq2ia 4963

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 2825	. . 3 ⊢ 𝐴 = 𝐴
2	1	ax-gen 1894	. 2 ⊢ ∀𝑥 𝐴 = 𝐴
3		mpteq2ia.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)
4	3	rgen 3131	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶
5		mpteq12f 4954	. 2 ⊢ ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
6	2, 4, 5	mp2an 683	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4  ∀wal 1654   = wceq 1656   ∈ wcel 2164  ∀wral 3117   ↦ cmpt 4952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-ral 3122  df-opab 4936  df-mpt 4953

This theorem is referenced by:  mpteq2i  4964  feqresmpt  6497  elfvmptrab  6554  fmptap  6688  offres  7423  resixpfo  8213  dfoi  8685  cantnflem1d  8862  cantnflem1  8863  dfceil2  12935  dfid5  14144  dfid6  14145  cnrecnv  14282  ackbijnn  14934  harmonic  14965  ege2le3  15192  eirrlem  15306  prmrec  15997  imasdsval2  16529  cayleylem1  18182  pmtrprfval  18257  gsumzsplit  18680  gsum2dlem2  18723  dmdprdsplitlem  18790  coe1sclmul  20012  coe1sclmul2  20014  frlmip  20484  mdetunilem9  20794  leordtvallem1  21385  leordtvallem2  21386  txkgen  21826  cnmpt1st  21842  cnmpt2nd  21843  tmdgsum  22269  tsmssplit  22325  cnfldnm  22952  expcn  23045  pcorev2  23197  pi1xfrcnv  23226  rrxip  23558  mbfi1flim  23889  itg2uba  23909  itg2cnlem1  23927  itg2cnlem2  23928  itgitg2  23972  itgss3  23980  itgless  23982  ibladdlem  23985  itgaddlem1  23988  iblabslem  23993  itggt0  24007  itgcn  24008  limcdif  24039  limcres  24049  cnplimc  24050  dvcobr  24108  dvexp  24115  dveflem  24141  dvef  24142  dvlip  24155  dvlipcn  24156  lhop  24178  tdeglem2  24220  plyid  24364  coeidp  24418  dgrid  24419  pserdvlem2  24581  abelth  24594  dvrelog  24782  logcn  24792  dvlog  24796  advlog  24799  advlogexp  24800  logtayl  24805  logccv  24808  dvcxp1  24883  dvsqrt  24885  dvcncxp1  24886  dvcnsqrt  24887  resqrtcn  24892  loglesqrt  24901  logblog  24932  dvatan  25075  leibpilem2  25081  leibpi  25082  efrlim  25109  sqrtlim  25112  amgmlem  25129  emcllem5  25139  lgamgulmlem2  25169  lgam1  25203  chtublem  25349  logfacrlim2  25364  bposlem6  25427  chto1lb  25580  vmadivsum  25584  dchrvmasumlema  25602  mulogsumlem  25633  logdivsum  25635  logsqvma2  25645  log2sumbnd  25646  selberglem1  25647  selberglem3  25649  selberg  25650  selberg2lem  25652  selberg2  25653  pntrmax  25666  pntrsumo1  25667  selbergr  25670  selbergs  25676  pnt2  25715  pnt  25716  ostth2  25739  ostth  25741  hilnormi  28564  bra0  29353  partfun  30012  zrhre  30597  qqhre  30598  eulerpartgbij  30968  plymulx  31161  faclim  32163  ptrest  33945  poimirlem19  33965  poimirlem20  33966  poimirlem30  33976  ovoliunnfl  33988  voliunnfl  33990  mbfposadd  33993  dvtan  33996  itg2addnclem  33997  ibladdnclem  34002  itgaddnclem1  34004  iblabsnclem  34009  itggt0cn  34018  ftc1anclem4  34024  ftc1anclem5  34025  ftc1anclem6  34026  ftc1anclem7  34027  ftc1anclem8  34028  dvasin  34032  dvacos  34033  areacirclem1  34036  arearect  38636  areaquad  38637  mptrcllem  38754  dfrcl2  38800  dfrcl3  38801  dftrcl3  38846  dfrtrcl3  38859  dfrtrcl4  38864  lhe4.4ex1a  39361  binomcxplemrat  39382  rnsnf  40171  feqresmptf  40228  limsupresre  40716  limsupvaluzmpt  40737  limsup10ex  40793  liminf10ex  40794  dvnprodlem1  40949  itgsin0pilem1  40953  wallispilem4  41072  wallispi2  41077  stirlinglem1  41078  stirlinglem3  41080  dirkercncflem2  41108  fourierdlem48  41158  fourierdlem49  41159  fourierdlem56  41166  fourierdlem57  41167  fourierdlem58  41168  fourierdlem62  41172  fourierdlem107  41217  fouriersw  41235  etransclem46  41284  sge0tsms  41381  sge0less  41393  sge0iun  41420  meadjun  41463  ovn02  41569  hoidmv1le  41595  hspmbllem2  41628  smflimsuplem3  41815