Theorem forn 5621

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 5386	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
2	1	simprbi 275	1 |- ( F : A -onto-> B -> ran F = B )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   ran crn 4777   Fn wfn 5375   -onto->wfo 5378

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-fo 5386

This theorem is used by:  dffo2  5622  foima  5623  fodmrnu  5626  f1imacnv  5659  foimacnv  5660  foun  5661  resdif  5664  fococnv2  5668  foelcdmi  5758  cbvfo  5994  cbvexfo  5995  isoini  6027  isoselem  6029  canth  6039  f1opw2  6299  focdmex  6348  mapfoss  6951  bren  7034  en1  7090  fopwdom  7140  mapen  7150  ssenen  7156  phplem4  7160  phplem4on  7173  ordiso2  7381  djuunr  7412  hashfacen  11306  ballotfilemro  13324  ennnfonelemrn  13368  imasival  13686  imasaddfnlemg  13694  xpsfrn  13730  imasmnd2  13818  imasgrp2  13972  imasrng  14362  imasring  14478  znf1o  15095  znleval  15097  znunit  15103  hmeontr  15539  fsumdvdsmul  16285