Theorem forn 5553

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 5324	. 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 1395   ran crn 4720   Fn wfn 5313   -onto->wfo 5316

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 5324

This theorem is referenced by:  dffo2  5554  foima  5555  fodmrnu  5558  f1imacnv  5591  foimacnv  5592  foun  5593  resdif  5596  fococnv2  5600  foelcdmi  5688  cbvfo  5915  cbvexfo  5916  isoini  5948  isoselem  5950  canth  5958  f1opw2  6218  focdmex  6266  bren  6903  en1  6959  fopwdom  7005  mapen  7015  ssenen  7020  phplem4  7024  phplem4on  7037  ordiso2  7213  djuunr  7244  hashfacen  11071  ennnfonelemrn  13006  imasival  13355  imasaddfnlemg  13363  xpsfrn  13399  imasmnd2  13501  imasgrp2  13663  imasrng  13935  imasring  14043  znf1o  14631  znleval  14633  znunit  14639  hmeontr  15003  fsumdvdsmul  15681