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