MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  feq2d Unicode version

Theorem feq2d 5723
Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
feq2d.1
Assertion
Ref Expression
feq2d

Proof of Theorem feq2d
StepHypRef Expression
1 feq2d.1 . 2
2 feq2 5719 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  -->wf 5589
This theorem is referenced by:  feq12d  5725  ffdm  5750  fsng  6070  fsnunf2  6110  issmo2  7039  qliftf  7418  elpm2r  7456  ralxpmap  7488  ordtypelem5  7968  axdc3lem3  8853  axdc3lem4  8854  fseq1p1m1  11781  fseq1m1p1  11782  seqf1o  12148  iswrdi  12552  wrdf  12553  snopiswrd  12556  ffz0iswrd  12568  wrdnval  12571  eqs1  12621  swrdf  12653  cats1un  12701  cshwf  12771  wrdlen2i  12884  wrd2pr2op  12885  wwlktovf  12894  rlimi  13336  rlimmptrcl  13430  lo1mptrcl  13444  o1mptrcl  13445  o1fsum  13627  ram0  14540  funcres  15265  curf2cl  15500  uncfcurf  15508  yonedalem4c  15546  intopsn  15882  gsumprval  15908  resmhm  15990  gsumwsubmcl  16006  gsumccat  16009  gsumwmhm  16013  frmdup1  16032  frmdup3lem  16034  isghm  16267  resghm  16283  subgga  16338  gasubg  16340  psgnunilem2  16520  sylow2blem2  16641  pj2f  16716  pj1ghm  16721  frgpupf  16791  frgpup3lem  16795  gsumval3OLD  16908  gsumval3  16911  gsummptfzcl  16996  dprdf2  17040  ablfaclem2  17137  ablfac2  17140  isabvd  17469  abvpropd  17491  mplasclf  18162  evlssca  18191  lply1binomsc  18349  cygznlem2a  18606  frgpcyg  18612  mat1dimelbas  18973  mat2pmatbas  19227  cpmadugsumlemF  19377  cnpf2  19751  lmcnp  19805  ptpjcn  20112  pt1hmeo  20307  cnextfres  20568  cnmpt2pc  21428  pi1addf  21547  pi1xfrf  21553  pi1cof  21559  mbfmptcl  22044  iblcnlem  22195  limcres  22290  cnplimc  22291  limccnp  22295  limccnp2  22296  limcun  22299  dvidlem  22319  cpnord  22338  dvaddf  22345  dvmulf  22346  dvcmulf  22348  dvcof  22351  dvcj  22353  dvrec  22358  dvmptcl  22362  dvcnvlem  22377  dvcnv  22378  rolle  22391  cmvth  22392  mvth  22393  dvlip  22394  dvlipcn  22395  c1lip2  22399  dv11cn  22402  dvivthlem1  22409  dvivthlem2  22410  dvivth  22411  dvne0  22412  lhop1lem  22414  lhop1  22415  lhop2  22416  lhop  22417  dvcnvrelem2  22419  taylthlem1  22768  taylthlem2  22769  ulmf2  22779  ulm2  22780  ulmdv  22798  pserdv  22824  rlimcxp  23303  o1cxp  23304  dchrptlem2  23540  axlowdimlem5  24249  axlowdimlem7  24251  axlowdimlem10  24254  uhgraun  24311  wrdumgra  24316  umgraf  24318  umgra1  24326  umgraun  24328  wlkelwrd  24530  2trllemH  24554  2trllemG  24560  is2wlk  24567  redwlk  24608  usgra2adedgwlkonALT  24616  usgra2wlkspthlem1  24619  usgra2wlkspthlem2  24620  fargshiftf  24636  3v3e3cycl1  24644  4cycl4v4e  24666  4cycl4dv  24667  4cycl4dv4e  24668  wlkiswwlk2lem3  24693  wlkiswwlk2  24697  vfwlkniswwlkn  24706  clwlkisclwwlklem2a  24785  clwlkisclwwlklem2  24786  clwlkfclwwlk2wrd  24840  clwlkf1clwwlklem3  24848  el2wlkonotlem  24862  eupai  24967  eupatrl  24968  eupa0  24974  eupares  24975  eupap1  24976  isgrpo  25198  elghomlem1OLD  25363  rngosn3  25428  vci  25441  isvclem  25470  vcoprnelem  25471  isnvlem  25503  ajfval  25724  locfinref  27844  1stmbfm  28231  2ndmbfm  28232  sibfof  28282  rrvf2  28387  signshf  28545  cvmliftmolem1  28726  cvmliftlem7  28736  cvmliftlem10  28739  cvmlift2lem9  28756  filnetlem4  30199  sdclem2  30235  sdclem1  30236  sdc  30237  fdc  30238  sstotbnd2  30270  mptelpm  31453  cncfuni  31689  cncfiooicclem1  31696  dvsubf  31709  dvdivf  31719  dvbdfbdioolem1  31725  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc1  31730  ioodvbdlimc2lem  31731  ioodvbdlimc2  31732  dvnprodlem3  31745  itgsubsticclem  31774  fourierdlem48  31937  fourierdlem49  31938  fourierdlem58  31947  fourierdlem59  31948  fourierdlem60  31949  fourierdlem61  31950  fourierdlem69  31958  fourierdlem75  31964  fourierdlem81  31970  fourierdlem89  31978  fourierdlem91  31980  fourierdlem97  31986  fourierdlem113  32002  2ffzoeq  32341  usgra2pthspth  32351  usgra2pthlem1  32353  usgra2pth  32354  uhgun  32380  resmgmhm  32486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2449  df-fn 5596  df-f 5597
  Copyright terms: Public domain W3C validator