Theorem funrel 5905

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

Syntax hints:   -> wi 4   C_ wss 3574   _I cid 5023   `'ccnv 5113   o. ccom 5118   Rel wrel 5119   Fun wfun 5882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-fun 5890

This theorem is referenced by:  0nelfun  5906  funeu  5913  nfunv  5921  funopg  5922  funssres  5930  funun  5932  fununfun  5934  fununi  5964  funcnvres2  5969  fnrel  5989  fcoi1  6078  f1orel  6140  funbrfv  6234  funbrfv2b  6240  funfv2  6266  funfvbrb  6330  fimacnvinrn  6348  fvn0ssdmfun  6350  funopsn  6413  funresdfunsn  6455  wfrrel  7420  tfrlem6  7478  tfr2b  7492  pmresg  7885  fundmen  8030  resfifsupp  8303  rankwflemb  8656  gruima  9624  structcnvcnv  15871  inviso1  16426  setciso  16741  pmtrsn  17939  00lsp  18981  edg0iedg0  25949  edg0iedg0OLD  25950  edg0usgr  26145  usgr1v0edg  26149  fmptcof2  29457  fgreu  29471  bnj1379  30901  fundmpss  31664  funsseq  31666  frrlem5b  31785  frrlem6  31789  nolt02o  31845  nosupbnd1  31860  nosupbnd2lem1  31861  nosupbnd2  31862  noetalem2  31864  noetalem3  31865  imageval  32037  imagesset  32060  cocnv  33520  frege124d  38053  frege129d  38055  frege133d  38057  funbrafv  41238  funbrafv2b  41239  rngciso  41982  rngcisoALTV  41994  ringciso  42033  ringcisoALTV  42057