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

Theorem forn 5140
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 4938 . 2  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
21simprbi 269 1  |-  ( F : A -onto-> B  ->  ran  F  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1285   ran crn 4372    Fn wfn 4927   -onto->wfo 4930
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105
This theorem depends on definitions:  df-bi 115  df-fo 4938
This theorem is referenced by:  dffo2  5141  foima  5142  fodmrnu  5145  f1imacnv  5174  foimacnv  5175  foun  5176  resdif  5179  fococnv2  5183  cbvfo  5456  cbvexfo  5457  isoini  5488  isoselem  5490  f1opw2  5737  fornex  5773  bren  6294  en1  6346  fopwdom  6380  phplem4  6390  phplem4on  6402  ordiso2  6505  focdmex  9811
  Copyright terms: Public domain W3C validator