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  7294  djuunr  7325  hashfacen  11163  ennnfonelemrn  13120  imasival  13469  imasaddfnlemg  13477  xpsfrn  13513  imasmnd2  13615  imasgrp2  13777  imasrng  14050  imasring  14158  znf1o  14747  znleval  14749  znunit  14755  hmeontr  15124  fsumdvdsmul  15805