Theorem forn 5486

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 5265	. 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 1364   ran crn 4665   Fn wfn 5254   -onto->wfo 5257

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 5265

This theorem is referenced by:  dffo2  5487  foima  5488  fodmrnu  5491  f1imacnv  5524  foimacnv  5525  foun  5526  resdif  5529  fococnv2  5533  foelcdmi  5616  cbvfo  5835  cbvexfo  5836  isoini  5868  isoselem  5870  canth  5878  f1opw2  6133  focdmex  6181  bren  6815  en1  6867  fopwdom  6906  mapen  6916  ssenen  6921  phplem4  6925  phplem4on  6937  ordiso2  7110  djuunr  7141  hashfacen  10945  ennnfonelemrn  12661  imasival  13008  imasaddfnlemg  13016  xpsfrn  13052  imasmnd2  13154  imasgrp2  13316  imasrng  13588  imasring  13696  znf1o  14283  znleval  14285  znunit  14291  hmeontr  14633  fsumdvdsmul  15311