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

Theorem funrel 5032
Description: A function is a relation. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
funrel (Fun 𝐴 → Rel 𝐴)

Proof of Theorem funrel
StepHypRef Expression
1 df-fun 5017 . 2 (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴𝐴) ⊆ I ))
21simplbi 268 1 (Fun 𝐴 → Rel 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 2999   I cid 4115  ccnv 4437  ccom 4442  Rel wrel 4443  Fun wfun 5009
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-fun 5017
This theorem is referenced by:  0nelfun  5033  funeu  5040  nfunv  5047  funopg  5048  funssres  5056  funun  5058  fununi  5082  funcnvres2  5089  funimaexg  5098  fnrel  5112  fcoi1  5191  f1orel  5256  funbrfv  5343  funbrfv2b  5349  fvmptss2  5379  funfvbrb  5412  fmptco  5464  funresdfunsnss  5500  elmpt2cl  5842  mpt2xopn0yelv  6004  tfrlem6  6081  funresdfunsndc  6265  pmresg  6433  fundmen  6523  hashinfom  10186  structcnvcnv  11510  istopon  11610
  Copyright terms: Public domain W3C validator