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

Theorem feq2d 5517
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 5513 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 178  =wceq 1687  -->wf 5386
This theorem is referenced by:  feq12d  5518  ffdm  5542  fsng  5851  fsnunf2  5886  issmo2  6769  qliftf  7149  elpm2r  7191  ralxpmap  7221  ordtypelem5  7683  axdc3lem3  8568  axdc3lem4  8569  fseq1p1m1  11475  fseq1m1p1  11476  seqf1o  11788  iswrdi  12180  wrdf  12181  snopiswrd  12184  ffz0iswrd  12196  wrdlenfi  12199  eqs1  12241  swrdf  12263  cats1un  12311  cshwf  12378  wrdlen2i  12487  wrd2pr2op  12488  rlimi  12932  rlimmptrcl  13026  lo1mptrcl  13040  o1mptrcl  13041  o1fsum  13216  ram0  14023  funcres  14746  curf2cl  14981  uncfcurf  14989  yonedalem4c  15027  resmhm  15426  gsumprval  15451  gsumwsubmcl  15453  gsumccat  15456  gsumwmhm  15460  frmdup1  15479  frmdup3  15481  isghm  15684  resghm  15700  subgga  15755  gasubg  15757  psgnunilem2  15938  sylow2blem2  16057  pj2f  16132  pj1ghm  16137  frgpupf  16207  frgpup3lem  16211  gsumval3  16317  gsummptfzcl  16354  dprdf2  16374  ablfaclem2  16453  ablfac2  16456  isabvd  16718  abvpropd  16740  mplasclf  17381  cygznlem2a  17708  frgpcyg  17714  cnpf2  18558  lmcnp  18612  ptpjcn  18888  pt1hmeo  19083  cnextfres  19344  cnmpt2pc  20200  pi1addf  20319  pi1xfrf  20325  pi1cof  20331  mbfmptcl  20815  iblcnlem  20966  limcres  21061  cnplimc  21062  limccnp  21066  limccnp2  21067  limcun  21070  dvidlem  21090  cpnord  21109  dvaddf  21116  dvmulf  21117  dvcmulf  21119  dvcof  21122  dvcj  21124  dvrec  21129  dvmptcl  21133  dvcnvlem  21148  dvcnv  21149  rolle  21162  cmvth  21163  mvth  21164  dvlip  21165  dvlipcn  21166  c1lip2  21170  dv11cn  21173  dvivthlem1  21180  dvivthlem2  21181  dvivth  21182  dvne0  21183  lhop1lem  21185  lhop1  21186  lhop2  21187  lhop  21188  dvcnvrelem2  21190  evlssca  21231  taylthlem1  21579  taylthlem2  21580  ulmf2  21590  ulm2  21591  ulmdv  21609  pserdv  21635  rlimcxp  22108  o1cxp  22109  dchrptlem2  22345  axlowdimlem5  22871  axlowdimlem7  22873  axlowdimlem10  22876  uhgraun  22924  wrdumgra  22929  umgraf  22931  umgra1  22939  umgraun  22941  2trllemH  23130  2trllemG  23136  is2wlk  23143  redwlk  23184  fargshiftf  23201  3v3e3cycl1  23209  4cycl4v4e  23231  4cycl4dv  23232  4cycl4dv4e  23233  eupai  23267  eupatrl  23268  eupa0  23274  eupares  23275  eupap1  23276  isgrpo  23362  elghomlem1  23527  rngosn3  23592  vci  23605  isvclem  23634  vcoprnelem  23635  isnvlem  23667  ajfval  23888  1stmbfm  26384  2ndmbfm  26385  sibfof  26429  rrvf2  26534  signshf  26692  cvmliftmolem1  26873  cvmliftlem7  26883  cvmliftlem10  26886  cvmlift2lem9  26903  filnetlem4  28273  sdclem2  28309  sdclem1  28310  sdc  28311  fdc  28312  sstotbnd2  28344  2ffzoeq  29888  wwlktovf  29925  wlkelwrd  29954  usgra2pthspth  29969  usgra2wlkspthlem1  29970  usgra2wlkspthlem2  29971  usgra2pthlem1  29974  usgra2pth  29975  wlkiswwlk2lem3  30001  wlkiswwlk2  30005  vfwlkniswwlkn  30014  el2wlkonotlem  30055  clwlkisclwwlklem2a  30121  clwlkisclwwlklem2  30122  wrdnval  30148  clwlkfclwwlk2wrd  30187  clwlkf1clwwlklem3  30195  gsumXval3  30465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-12 1785  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-an 364  df-ex 1582  df-cleq 2415  df-fn 5393  df-f 5394
  Copyright terms: Public domain W3C validator