Theorem forn 5523

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 5296	. 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 4694   Fn wfn 5285   -onto->wfo 5288

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 5296

This theorem is referenced by:  dffo2  5524  foima  5525  fodmrnu  5528  f1imacnv  5561  foimacnv  5562  foun  5563  resdif  5566  fococnv2  5570  foelcdmi  5654  cbvfo  5877  cbvexfo  5878  isoini  5910  isoselem  5912  canth  5920  f1opw2  6175  focdmex  6223  bren  6858  en1  6914  fopwdom  6958  mapen  6968  ssenen  6973  phplem4  6977  phplem4on  6990  ordiso2  7163  djuunr  7194  hashfacen  11018  ennnfonelemrn  12905  imasival  13253  imasaddfnlemg  13261  xpsfrn  13297  imasmnd2  13399  imasgrp2  13561  imasrng  13833  imasring  13941  znf1o  14528  znleval  14530  znunit  14536  hmeontr  14900  fsumdvdsmul  15578