ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  forn Structured version   Unicode version

Theorem forn 5052
Description: The codomain of an onto function is its range. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
forn  F : -onto->  ran 
F

Proof of Theorem forn
StepHypRef Expression
1 df-fo 4851 . 2  F : -onto->  F  Fn  ran  F
21simprbi 260 1  F : -onto->  ran 
F
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1242   ran crn 4289    Fn wfn 4840   -onto->wfo 4843
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100
This theorem depends on definitions:  df-bi 110  df-fo 4851
This theorem is referenced by:  dffo2  5053  foima  5054  fodmrnu  5057  f1imacnv  5086  foimacnv  5087  foun  5088  resdif  5091  fococnv2  5095  cbvfo  5368  cbvexfo  5369  isoini  5400  isoselem  5402  f1opw2  5648  fornex  5684  bren  6164  en1  6215  fopwdom  6246
  Copyright terms: Public domain W3C validator