Theorem forn 5460

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 5241	. 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 4645   Fn wfn 5230   -onto->wfo 5233

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 5241

This theorem is referenced by:  dffo2  5461  foima  5462  fodmrnu  5465  f1imacnv  5497  foimacnv  5498  foun  5499  resdif  5502  fococnv2  5506  foelcdmi  5589  cbvfo  5807  cbvexfo  5808  isoini  5840  isoselem  5842  canth  5850  f1opw2  6100  focdmex  6140  bren  6773  en1  6825  fopwdom  6864  mapen  6874  ssenen  6879  phplem4  6883  phplem4on  6895  ordiso2  7064  djuunr  7095  hashfacen  10848  ennnfonelemrn  12470  imasival  12783  imasaddfnlemg  12791  xpsfrn  12826  imasgrp2  13052  imasrng  13310  imasring  13414  hmeontr  14273