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

Theorem frn 5052
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 4906 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
21simprbi 260 1  |-  ( F : A --> B  ->  ran  F  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 2917   ran crn 4346    Fn wfn 4897   -->wf 4898
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100
This theorem depends on definitions:  df-bi 110  df-f 4906
This theorem is referenced by:  fco2  5057  fssxp  5058  fimacnvdisj  5074  f00  5081  fun11iun  5147  fimacnv  5296  ffvelrn  5300  f1ompt  5320  fnfvrnss  5325  rnmptss  5326  fliftrel  5432  f1dmex  5743  fo1stresm  5788  fo2ndresm  5789  1stcof  5790  2ndcof  5791  fo2ndf  5848  tposf2  5883  iunon  5899  smores2  5909  f1imaen2g  6273  phplem4dom  6324  unirnioo  8842
  Copyright terms: Public domain W3C validator