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

Theorem forn 5236
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 5021 . 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 1289   ran crn 4439    Fn wfn 5010   -onto->wfo 5013
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 5021
This theorem is referenced by:  dffo2  5237  foima  5238  fodmrnu  5241  f1imacnv  5270  foimacnv  5271  foun  5272  resdif  5275  fococnv2  5279  cbvfo  5564  cbvexfo  5565  isoini  5597  isoselem  5599  f1opw2  5850  fornex  5886  bren  6464  en1  6516  fopwdom  6552  mapen  6562  ssenen  6567  phplem4  6571  phplem4on  6583  ordiso2  6728  djuunr  6758  focdmex  10195  hashfacen  10241
  Copyright terms: Public domain W3C validator