Theorem funrel 5297

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 5282	. 2 |- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
2	1	simplbi 274	1 |- ( Fun A -> Rel A )

Syntax hints:   -> wi 4   C_ wss 3170   _I cid 4343   `'ccnv 4682   o. ccom 4687   Rel wrel 4688   Fun wfun 5274

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

This theorem depends on definitions:  df-bi 117  df-fun 5282

This theorem is referenced by:  0nelfun  5298  funeu  5305  nfunv  5313  funopg  5314  funssres  5322  funun  5324  fununfun  5326  fununi  5351  funcnvres2  5358  funimaexg  5367  fnrel  5381  fcoi1  5468  f1orel  5537  funbrfv  5630  funbrfv2b  5636  fvmptss2  5667  mptrcl  5675  elfvmptrab1  5687  funfvbrb  5706  fmptco  5759  funopsn  5775  funresdfunsnss  5800  elmpocl  6154  funexw  6210  mpoxopn0yelv  6338  tfrlem6  6415  funresdfunsndc  6605  pmresg  6776  fundmen  6912  caseinl  7208  caseinr  7209  axaddf  8001  axmulf  8002  hashinfom  10945  4sqlemffi  12794  structcnvcnv  12923  lidlmex  14312  istopon  14560  eltg4i  14602  eltg3  14604  tg1  14606  tg2  14607  tgclb  14612  lmrcl  14738  1vgrex  15694  edg0iedg0g  15737  umgrnloopvv  15785