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

Theorem fnrel 5296
Description: A function with domain is a relation. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
fnrel (𝐹 Fn 𝐴 → Rel 𝐹)

Proof of Theorem fnrel
StepHypRef Expression
1 fnfun 5295 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
2 funrel 5215 . 2 (Fun 𝐹 → Rel 𝐹)
31, 2syl 14 1 (𝐹 Fn 𝐴 → Rel 𝐹)
Colors of variables: wff set class
Syntax hints:  wi 4  Rel wrel 4616  Fun wfun 5192   Fn wfn 5193
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-fun 5200  df-fn 5201
This theorem is referenced by:  fnbr  5300  fnresdm  5307  fn0  5317  frel  5352  fcoi2  5379  f1rel  5407  f1ocnv  5455  dffn5im  5542  fnex  5718  fnexALT  6090  basmex  12474  basmexd  12475  ismgmn0  12612  istps  12824  topontopn  12829  cldrcl  12896  neiss2  12936
  Copyright terms: Public domain W3C validator