Theorem forn 5595

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 5360	. 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 1398   ran crn 4752   Fn wfn 5349   -onto->wfo 5352

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 5360

This theorem is referenced by:  dffo2  5596  foima  5597  fodmrnu  5600  f1imacnv  5633  foimacnv  5634  foun  5635  resdif  5638  fococnv2  5642  foelcdmi  5731  cbvfo  5960  cbvexfo  5961  isoini  5993  isoselem  5995  canth  6003  f1opw2  6263  focdmex  6310  bren  6985  en1  7041  fopwdom  7091  mapen  7101  ssenen  7107  phplem4  7111  phplem4on  7124  ordiso2  7328  djuunr  7359  hashfacen  11212  ennnfonelemrn  13187  imasival  13536  imasaddfnlemg  13544  xpsfrn  13580  imasmnd2  13682  imasgrp2  13844  imasrng  14117  imasring  14225  znf1o  14816  znleval  14818  znunit  14824  hmeontr  15195  fsumdvdsmul  15876