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

Theorem funrel 4947
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 4932 . 2 (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴𝐴) ⊆ I ))
21simplbi 263 1 (Fun 𝐴 → Rel 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 2945   I cid 4053  ccnv 4372  ccom 4377  Rel wrel 4378  Fun wfun 4924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114  df-fun 4932
This theorem is referenced by:  funeu  4954  nfunv  4961  funopg  4962  funssres  4970  funun  4972  fununi  4995  funcnvres2  5002  funimaexg  5011  fnrel  5025  fcoi1  5098  f1orel  5157  funbrfv  5240  funbrfv2b  5246  fvmptss2  5275  funfvbrb  5308  fmptco  5358  elmpt2cl  5726  mpt2xopn0yelv  5885  tfrlem6  5963  fundmen  6317
  Copyright terms: Public domain W3C validator