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

Theorem forn 5318
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 5099 . 2  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
21simprbi 273 1  |-  ( F : A -onto-> B  ->  ran  F  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316   ran crn 4510    Fn wfn 5088   -onto->wfo 5091
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem depends on definitions:  df-bi 116  df-fo 5099
This theorem is referenced by:  dffo2  5319  foima  5320  fodmrnu  5323  f1imacnv  5352  foimacnv  5353  foun  5354  resdif  5357  fococnv2  5361  cbvfo  5654  cbvexfo  5655  isoini  5687  isoselem  5689  f1opw2  5944  fornex  5981  bren  6609  en1  6661  fopwdom  6698  mapen  6708  ssenen  6713  phplem4  6717  phplem4on  6729  ordiso2  6888  djuunr  6919  focdmex  10501  hashfacen  10547  ennnfonelemrn  11859  hmeontr  12409
  Copyright terms: Public domain W3C validator