Theorem forn 5551

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 5324	. 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 1395   ran crn 4720   Fn wfn 5313   -onto->wfo 5316

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 5324

This theorem is referenced by:  dffo2  5552  foima  5553  fodmrnu  5556  f1imacnv  5589  foimacnv  5590  foun  5591  resdif  5594  fococnv2  5598  foelcdmi  5686  cbvfo  5909  cbvexfo  5910  isoini  5942  isoselem  5944  canth  5952  f1opw2  6212  focdmex  6260  bren  6895  en1  6951  fopwdom  6997  mapen  7007  ssenen  7012  phplem4  7016  phplem4on  7029  ordiso2  7202  djuunr  7233  hashfacen  11058  ennnfonelemrn  12990  imasival  13339  imasaddfnlemg  13347  xpsfrn  13383  imasmnd2  13485  imasgrp2  13647  imasrng  13919  imasring  14027  znf1o  14615  znleval  14617  znunit  14623  hmeontr  14987  fsumdvdsmul  15665