Theorem forn 5484

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  5485  foima  5486  fodmrnu  5489  f1imacnv  5522  foimacnv  5523  foun  5524  resdif  5527  fococnv2  5531  foelcdmi  5614  cbvfo  5833  cbvexfo  5834  isoini  5866  isoselem  5868  canth  5876  f1opw2  6130  focdmex  6173  bren  6807  en1  6859  fopwdom  6898  mapen  6908  ssenen  6913  phplem4  6917  phplem4on  6929  ordiso2  7102  djuunr  7133  hashfacen  10930  ennnfonelemrn  12646  imasival  12959  imasaddfnlemg  12967  xpsfrn  13003  imasgrp2  13250  imasrng  13522  imasring  13630  znf1o  14217  znleval  14219  znunit  14225  hmeontr  14559  fsumdvdsmul  15237