ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  forn Unicode version

Theorem forn 5460
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
StepHypRef Expression
1 df-fo 5241 . 2  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
21simprbi 275 1  |-  ( F : A -onto-> B  ->  ran  F  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1364   ran crn 4645    Fn wfn 5230   -onto->wfo 5233
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 5241
This theorem is referenced by:  dffo2  5461  foima  5462  fodmrnu  5465  f1imacnv  5497  foimacnv  5498  foun  5499  resdif  5502  fococnv2  5506  foelcdmi  5589  cbvfo  5807  cbvexfo  5808  isoini  5840  isoselem  5842  canth  5850  f1opw2  6100  focdmex  6140  bren  6773  en1  6825  fopwdom  6864  mapen  6874  ssenen  6879  phplem4  6883  phplem4on  6895  ordiso2  7064  djuunr  7095  hashfacen  10848  ennnfonelemrn  12470  imasival  12783  imasaddfnlemg  12791  xpsfrn  12826  imasgrp2  13052  imasrng  13310  imasring  13414  hmeontr  14273
  Copyright terms: Public domain W3C validator