Theorem forn 5503

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 5278	. 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 1373   ran crn 4677   Fn wfn 5267   -onto->wfo 5270

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 5278

This theorem is referenced by:  dffo2  5504  foima  5505  fodmrnu  5508  f1imacnv  5541  foimacnv  5542  foun  5543  resdif  5546  fococnv2  5550  foelcdmi  5633  cbvfo  5856  cbvexfo  5857  isoini  5889  isoselem  5891  canth  5899  f1opw2  6154  focdmex  6202  bren  6837  en1  6893  fopwdom  6935  mapen  6945  ssenen  6950  phplem4  6954  phplem4on  6966  ordiso2  7139  djuunr  7170  hashfacen  10983  ennnfonelemrn  12823  imasival  13171  imasaddfnlemg  13179  xpsfrn  13215  imasmnd2  13317  imasgrp2  13479  imasrng  13751  imasring  13859  znf1o  14446  znleval  14448  znunit  14454  hmeontr  14818  fsumdvdsmul  15496