Theorem funrel 5343

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 5328	. 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 3200   _I cid 4385   `'ccnv 4724   o. ccom 4729   Rel wrel 4730   Fun wfun 5320

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 5328

This theorem is referenced by:  0nelfun  5344  funeu  5351  nfunv  5359  funopg  5360  funssres  5369  funun  5371  fununfun  5373  fununi  5398  funcnvres2  5405  funimaexg  5414  fnrel  5428  fcoi1  5517  f1orel  5586  funbrfv  5682  funbrfv2b  5690  fvmptss2  5721  mptrcl  5729  elfvmptrab1  5741  funfvbrb  5760  fmptco  5813  funopsn  5829  funresdfunsnss  5856  elmpocl  6216  relmptopab  6223  funexw  6273  elmpom  6402  mpoxopn0yelv  6404  tfrlem6  6481  funresdfunsndc  6673  pmresg  6844  fundmen  6980  caseinl  7289  caseinr  7290  axaddf  8087  axmulf  8088  hashinfom  11039  4sqlemffi  12968  structcnvcnv  13097  lidlmex  14488  istopon  14736  eltg4i  14778  eltg3  14780  tg1  14782  tg2  14783  tgclb  14788  lmrcl  14915  1vgrex  15870  edg0iedg0g  15916  umgrnloopv  15964  edg0usgr  16097