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

Theorem frn 5077
Description: The range of a mapping. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
frn  |-  ( F : A --> B  ->  ran  F  C_  B )

Proof of Theorem frn
StepHypRef Expression
1 df-f 4930 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
21simprbi 269 1  |-  ( F : A --> B  ->  ran  F  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 2974   ran crn 4366    Fn wfn 4921   -->wf 4922
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105
This theorem depends on definitions:  df-bi 115  df-f 4930
This theorem is referenced by:  fco2  5082  fssxp  5083  fimacnvdisj  5099  f00  5106  fun11iun  5172  fimacnv  5322  ffvelrn  5326  f1ompt  5346  fnfvrnss  5351  rnmptss  5352  fliftrel  5457  f1dmex  5768  fo1stresm  5813  fo2ndresm  5814  1stcof  5815  2ndcof  5816  fo2ndf  5873  tposf2  5911  iunon  5927  smores2  5937  f1imaen2g  6332  phplem4dom  6387  unirnioo  9061  frecuzrdgdomlem  9488  frecuzrdgfunlem  9490  frecuzrdgtclt  9492
  Copyright terms: Public domain W3C validator