Theorem mpteq2ia 5160

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 2824	. . 3 ⊢ 𝐴 = 𝐴
2	1	ax-gen 1795	. 2 ⊢ ∀𝑥 𝐴 = 𝐴
3		mpteq2ia.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)
4	3	rgen 3151	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶
5		mpteq12f 5152	. 2 ⊢ ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
6	2, 4, 5	mp2an 690	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4  ∀wal 1534   = wceq 1536   ∈ wcel 2113  ∀wral 3141   ↦ cmpt 5149

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-ral 3146  df-opab 5132  df-mpt 5150

This theorem is referenced by:  mpteq2i  5161  feqresmpt  6737  elfvmptrab  6799  fmptap  6935  offres  7687  resixpfo  8503  dfoi  8978  cantnflem1d  9154  cantnflem1  9155  dfceil2  13212  dfid5  14389  dfid6  14390  cnrecnv  14527  ackbijnn  15186  harmonic  15217  ege2le3  15446  eirrlem  15560  prmrec  16261  imasdsval2  16792  smndex1iidm  18069  smndex2dlinvh  18085  cayleylem1  18543  pmtrprfval  18618  gsumzsplit  19050  gsum2dlem2  19094  dmdprdsplitlem  19162  coe1sclmul  20453  coe1sclmul2  20455  frlmip  20925  mdetunilem9  21232  leordtvallem1  21821  leordtvallem2  21822  txkgen  22263  cnmpt1st  22279  cnmpt2nd  22280  tmdgsum  22706  tsmssplit  22763  cnfldnm  23390  expcn  23483  pcorev2  23635  pi1xfrcnv  23664  rrxip  23996  mbfi1flim  24327  itg2uba  24347  itg2cnlem1  24365  itg2cnlem2  24366  itgitg2  24410  itgss3  24418  itgless  24420  ibladdlem  24423  itgaddlem1  24426  iblabslem  24431  itggt0  24445  itgcn  24446  limcdif  24477  limcres  24487  cnplimc  24488  dvcobr  24546  dvexp  24553  dveflem  24579  dvef  24580  dvlip  24593  dvlipcn  24594  lhop  24616  tdeglem2  24658  plyid  24802  coeidp  24856  dgrid  24857  pserdvlem2  25019  abelth  25032  dvrelog  25223  logcn  25233  dvlog  25237  advlog  25240  advlogexp  25241  logtayl  25246  logccv  25249  dvcxp1  25324  dvsqrt  25326  dvcncxp1  25327  dvcnsqrt  25328  resqrtcn  25333  loglesqrt  25342  logblog  25373  dvatan  25516  leibpilem2  25522  leibpi  25523  efrlim  25550  sqrtlim  25553  amgmlem  25570  emcllem5  25580  lgamgulmlem2  25610  lgam1  25644  chtublem  25790  logfacrlim2  25805  bposlem6  25868  chto1lb  26057  vmadivsum  26061  dchrvmasumlema  26079  mulogsumlem  26110  logdivsum  26112  logsqvma2  26122  log2sumbnd  26123  selberglem1  26124  selberglem3  26126  selberg  26127  selberg2lem  26129  selberg2  26130  pntrmax  26143  pntrsumo1  26144  selbergr  26147  selbergs  26153  pnt2  26192  pnt  26193  ostth2  26216  ostth  26218  hilnormi  28943  bra0  29730  partfun  30424  zrhre  31264  qqhre  31265  eulerpartgbij  31634  plymulx  31822  elmrsubrn  32771  faclim  32982  ptrest  34895  poimirlem19  34915  poimirlem20  34916  poimirlem30  34926  ovoliunnfl  34938  voliunnfl  34940  mbfposadd  34943  dvtan  34946  itg2addnclem  34947  ibladdnclem  34952  itgaddnclem1  34954  iblabsnclem  34959  itggt0cn  34968  ftc1anclem4  34974  ftc1anclem5  34975  ftc1anclem6  34976  ftc1anclem7  34977  ftc1anclem8  34978  dvasin  34982  dvacos  34983  areacirclem1  34986  arearect  39828  areaquad  39829  mptrcllem  39979  dfrcl2  40025  dfrcl3  40026  dftrcl3  40071  dfrtrcl3  40084  dfrtrcl4  40089  lhe4.4ex1a  40667  binomcxplemrat  40688  rnsnf  41450  feqresmptf  41505  limsupresre  41983  limsupvaluzmpt  42004  limsup10ex  42060  liminf10ex  42061  dvnprodlem1  42237  itgsin0pilem1  42241  wallispilem4  42360  wallispi2  42365  stirlinglem1  42366  stirlinglem3  42368  dirkercncflem2  42396  fourierdlem48  42446  fourierdlem49  42447  fourierdlem56  42454  fourierdlem57  42455  fourierdlem58  42456  fourierdlem62  42460  fourierdlem107  42505  fouriersw  42523  etransclem46  42572  sge0tsms  42669  sge0less  42681  sge0iun  42708  meadjun  42751  ovn02  42857  hoidmv1le  42883  hspmbllem2  42916  smflimsuplem3  43103