Theorem funrel 5098

Description: A function is a relation. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
funrel	|- ( Fun A -> Rel A )

Proof of Theorem funrel

Step	Hyp	Ref	Expression
1		df-fun 5083	. 2 |- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
2	1	simplbi 270	1 |- ( Fun A -> Rel A )

Syntax hints:   -> wi 4   C_ wss 3037   _I cid 4170   `'ccnv 4498   o. ccom 4503   Rel wrel 4504   Fun wfun 5075

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-fun 5083

This theorem is referenced by:  0nelfun  5099  funeu  5106  nfunv  5114  funopg  5115  funssres  5123  funun  5125  fununi  5149  funcnvres2  5156  funimaexg  5165  fnrel  5179  fcoi1  5261  f1orel  5326  funbrfv  5414  funbrfv2b  5420  fvmptss2  5450  mptrcl  5457  elfvmptrab1  5469  funfvbrb  5487  fmptco  5540  funresdfunsnss  5577  elmpocl  5922  mpoxopn0yelv  6090  tfrlem6  6167  funresdfunsndc  6356  pmresg  6524  fundmen  6654  caseinl  6928  caseinr  6929  axaddf  7603  axmulf  7604  hashinfom  10417  structcnvcnv  11818  istopon  12023  eltg4i  12067  eltg3  12069  tg1  12071  tg2  12072  tgclb  12077  lmrcl  12203