New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  forn GIF version

Theorem forn 5272
 Description: The codomain of an onto function is its range. (Contributed by set.mm contributors, 3-Aug-1994.)
Assertion
Ref Expression
forn (F:AontoB → ran F = B)

Proof of Theorem forn
StepHypRef Expression
1 df-fo 4793 . 2 (F:AontoB ↔ (F Fn A ran F = B))
21simprbi 450 1 (F:AontoB → ran F = B)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1642  ran crn 4773   Fn wfn 4776  –onto→wfo 4779 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 177  df-an 360  df-fo 4793 This theorem is referenced by:  dffo2  5273  foima  5274  fodmrnu  5277  f1imacnv  5302  foimacnv  5303  resdif  5306  f1ococnv2  5309  dffo4  5423  isoini  5497  bren  6030  enpw1  6062  enmap1lem5  6073  nenpw1pwlem2  6085  ncdisjun  6136  1cnc  6139  sbthlem3  6205
 Copyright terms: Public domain W3C validator