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