Theorem forn 5571

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 5339	. 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 4732   Fn wfn 5328   -onto->wfo 5331

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 5339

This theorem is referenced by:  dffo2  5572  foima  5573  fodmrnu  5576  f1imacnv  5609  foimacnv  5610  foun  5611  resdif  5614  fococnv2  5618  foelcdmi  5707  cbvfo  5936  cbvexfo  5937  isoini  5969  isoselem  5971  canth  5979  f1opw2  6239  focdmex  6286  bren  6960  en1  7016  fopwdom  7065  mapen  7075  ssenen  7080  phplem4  7084  phplem4on  7097  ordiso2  7277  djuunr  7308  hashfacen  11144  ennnfonelemrn  13101  imasival  13450  imasaddfnlemg  13458  xpsfrn  13494  imasmnd2  13596  imasgrp2  13758  imasrng  14031  imasring  14139  znf1o  14727  znleval  14729  znunit  14735  hmeontr  15104  fsumdvdsmul  15782