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

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

Proof of Theorem forn
StepHypRef Expression
1 df-fo 4908 . 2  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
21simprbi 260 1  |-  ( F : A -onto-> B  ->  ran  F  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1243   ran crn 4346    Fn wfn 4897   -onto->wfo 4900
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 4908
This theorem is referenced by:  dffo2  5110  foima  5111  fodmrnu  5114  f1imacnv  5143  foimacnv  5144  foun  5145  resdif  5148  fococnv2  5152  cbvfo  5425  cbvexfo  5426  isoini  5457  isoselem  5459  f1opw2  5706  fornex  5742  bren  6228  en1  6279  fopwdom  6310  phplem4  6318  phplem4on  6329  ordiso2  6355
  Copyright terms: Public domain W3C validator