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

Theorem funrel 5140
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 5125 . 2 (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴𝐴) ⊆ I ))
21simplbi 272 1 (Fun 𝐴 → Rel 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 3071   I cid 4210  ccnv 4538  ccom 4543  Rel wrel 4544  Fun wfun 5117
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 5125
This theorem is referenced by:  0nelfun  5141  funeu  5148  nfunv  5156  funopg  5157  funssres  5165  funun  5167  fununi  5191  funcnvres2  5198  funimaexg  5207  fnrel  5221  fcoi1  5303  f1orel  5370  funbrfv  5460  funbrfv2b  5466  fvmptss2  5496  mptrcl  5503  elfvmptrab1  5515  funfvbrb  5533  fmptco  5586  funresdfunsnss  5623  elmpocl  5968  mpoxopn0yelv  6136  tfrlem6  6213  funresdfunsndc  6402  pmresg  6570  fundmen  6700  caseinl  6976  caseinr  6977  axaddf  7683  axmulf  7684  hashinfom  10531  structcnvcnv  11985  istopon  12190  eltg4i  12234  eltg3  12236  tg1  12238  tg2  12239  tgclb  12244  lmrcl  12370
  Copyright terms: Public domain W3C validator