Theorem forn 5443

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

Step	Hyp	Ref	Expression
1		df-fo 5224	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
2	1	simprbi 275	1 |- ( F : A -onto-> B -> ran F = B )

Syntax hints:   -> wi 4   = wceq 1353   ran crn 4629   Fn wfn 5213   -onto->wfo 5216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-fo 5224

This theorem is referenced by:  dffo2  5444  foima  5445  fodmrnu  5448  f1imacnv  5480  foimacnv  5481  foun  5482  resdif  5485  fococnv2  5489  foelcdmi  5570  cbvfo  5788  cbvexfo  5789  isoini  5821  isoselem  5823  canth  5831  f1opw2  6079  focdmex  6118  bren  6749  en1  6801  fopwdom  6838  mapen  6848  ssenen  6853  phplem4  6857  phplem4on  6869  ordiso2  7036  djuunr  7067  hashfacen  10818  ennnfonelemrn  12422  imasival  12732  imasaddfnlemg  12740  xpsfrn  12774  hmeontr  13898