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

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

Proof of Theorem frn
StepHypRef Expression
1 df-f 4849 . 2  F : -->  F  Fn  ran  F 
C_
21simprbi 260 1  F : -->  ran 
F  C_
Colors of variables: wff set class
Syntax hints:   wi 4    C_ wss 2911   ran crn 4289    Fn wfn 4840   -->wf 4841
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 4849
This theorem is referenced by:  fco2  5000  fssxp  5001  fimacnvdisj  5017  f00  5024  fun11iun  5090  fimacnv  5239  ffvelrn  5243  f1ompt  5263  fnfvrnss  5268  rnmptss  5269  fliftrel  5375  f1dmex  5685  fo1stresm  5730  fo2ndresm  5731  1stcof  5732  2ndcof  5733  fo2ndf  5790  tposf2  5824  iunon  5840  smores2  5850  f1imaen2g  6209  unirnioo  8612
  Copyright terms: Public domain W3C validator