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

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

Proof of Theorem funrel
StepHypRef Expression
1 df-fun 4847 . 2 (Fun A ↔ (Rel A (AA) ⊆ I ))
21simplbi 259 1 (Fun A → Rel A)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 2911   I cid 4016  ccnv 4287  ccom 4292  Rel wrel 4293  Fun wfun 4839
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110  df-fun 4847
This theorem is referenced by:  funeu  4869  nfunv  4876  funopg  4877  funssres  4885  funun  4887  fununi  4910  funcnvres2  4917  funimaexg  4926  fnrel  4940  fcoi1  5013  f1orel  5072  funbrfv  5155  funbrfv2b  5161  fvmptss2  5190  funfvbrb  5223  fmptco  5273  elmpt2cl  5640  mpt2xopn0yelv  5795  tfrlem6  5873  fundmen  6222
  Copyright terms: Public domain W3C validator