Theorem forn 5562

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 5332	. 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 1397   ran crn 4726   Fn wfn 5321   -onto->wfo 5324

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 5332

This theorem is referenced by:  dffo2  5563  foima  5564  fodmrnu  5567  f1imacnv  5600  foimacnv  5601  foun  5602  resdif  5605  fococnv2  5609  foelcdmi  5698  cbvfo  5926  cbvexfo  5927  isoini  5959  isoselem  5961  canth  5969  f1opw2  6229  focdmex  6277  bren  6917  en1  6973  fopwdom  7022  mapen  7032  ssenen  7037  phplem4  7041  phplem4on  7054  ordiso2  7234  djuunr  7265  hashfacen  11101  ennnfonelemrn  13058  imasival  13407  imasaddfnlemg  13415  xpsfrn  13451  imasmnd2  13553  imasgrp2  13715  imasrng  13988  imasring  14096  znf1o  14684  znleval  14686  znunit  14692  hmeontr  15056  fsumdvdsmul  15734