Theorem forn 5501

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 5277	. 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 1373   ran crn 4676   Fn wfn 5266   -onto->wfo 5269

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 5277

This theorem is referenced by:  dffo2  5502  foima  5503  fodmrnu  5506  f1imacnv  5539  foimacnv  5540  foun  5541  resdif  5544  fococnv2  5548  foelcdmi  5631  cbvfo  5854  cbvexfo  5855  isoini  5887  isoselem  5889  canth  5897  f1opw2  6152  focdmex  6200  bren  6835  en1  6891  fopwdom  6933  mapen  6943  ssenen  6948  phplem4  6952  phplem4on  6964  ordiso2  7137  djuunr  7168  hashfacen  10981  ennnfonelemrn  12790  imasival  13138  imasaddfnlemg  13146  xpsfrn  13182  imasmnd2  13284  imasgrp2  13446  imasrng  13718  imasring  13826  znf1o  14413  znleval  14415  znunit  14421  hmeontr  14785  fsumdvdsmul  15463