Theorem funrel 5368

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 5353	. 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 3210   _I cid 4408   `'ccnv 4747   o. ccom 4752   Rel wrel 4753   Fun wfun 5345

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 5353

This theorem is referenced by:  0nelfun  5369  funeu  5376  nfunv  5384  funopg  5385  funssres  5394  funun  5396  fununfun  5398  fununi  5423  funcnvres2  5430  funimaexg  5439  fnrel  5453  fcoi1  5546  f1orel  5616  funbrfv  5712  funbrfv2b  5720  fvmptss2  5751  mptrcl  5759  elfvmptrab1  5771  funfvbrb  5790  fmptco  5842  funopsn  5859  funresdfunsnss  5886  elmpocl  6248  relmptopab  6255  funexw  6304  elmpom  6433  mpoxopn0yelv  6469  tfrlem6  6546  funresdfunsndc  6738  pmresg  6909  fundmen  7046  caseinl  7381  caseinr  7382  axaddf  8182  axmulf  8183  hashinfom  11139  4sqlemffi  13090  structcnvcnv  13220  lidlmex  14615  istopon  14870  eltg4i  14912  eltg3  14914  tg1  14916  tg2  14917  tgclb  14922  lmrcl  15049  1vgrex  16007  edg0iedg0g  16053  umgrnloopv  16101  edg0usgr  16234