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

Theorem dffo2 5804
 Description: Alternate definition of an onto function. (Contributed by NM, 22-Mar-2006.)
Assertion
Ref Expression
dffo2

Proof of Theorem dffo2
StepHypRef Expression
1 fof 5800 . . 3
2 forn 5803 . . 3
31, 2jca 532 . 2
4 ffn 5736 . . 3
5 df-fo 5599 . . . 4
65biimpri 206 . . 3
74, 6sylan 471 . 2
83, 7impbii 188 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  /\wa 369  =wceq 1395  rancrn 5005  Fnwfn 5588  -->wf 5589  -onto->wfo 5591 This theorem is referenced by:  foco  5810  foconst  5811  dff1o5  5830  dffo3  6046  dffo4  6047  exfo  6049  fo1stres  6824  fo2ndres  6825  fo2ndf  6907  cantnf  8133  cantnfOLD  8155  hsmexlem2  8828  1fv  11821  setcepi  15415  odf1o1  16592  efgsfo  16757  pjfo  18746  xrhmeo  21446  fargshiftfo  24638  grpofo  25201  cnpcon  28675  lnmepi  31031 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-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489  df-f 5597  df-fo 5599
 Copyright terms: Public domain W3C validator