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

Theorem fnrel 5333
Description: A function with domain is a relation. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
fnrel  |-  ( F  Fn  A  ->  Rel  F )

Proof of Theorem fnrel
StepHypRef Expression
1 fnfun 5332 . 2  |-  ( F  Fn  A  ->  Fun  F )
2 funrel 5252 . 2  |-  ( Fun 
F  ->  Rel  F )
31, 2syl 14 1  |-  ( F  Fn  A  ->  Rel  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4   Rel wrel 4649   Fun wfun 5229    Fn wfn 5230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117  df-fun 5237  df-fn 5238
This theorem is referenced by:  fnbr  5337  fnresdm  5344  fn0  5354  frel  5389  fcoi2  5416  f1rel  5444  f1ocnv  5493  dffn5im  5581  fnex  5758  fnexALT  6135  basmex  12570  basmexd  12571  ismgmn0  12831  istps  13984  topontopn  13989  cldrcl  14054  neiss2  14094
  Copyright terms: Public domain W3C validator