Theorem funrel 5397

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

This proof depends on syntax axioms:   -> wi 4   C_ wss 3220   _I cid 4435   `'ccnv 4775   o. ccom 4780   Rel wrel 4781   Fun wfun 5374

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-fun 5382

This theorem is used by:  0nelfun  5398  funeu  5405  nfunv  5413  funopg  5414  funssres  5423  funun  5425  fununfun  5427  fununi  5452  funcnvres2  5459  funimaexg  5468  fnrel  5482  fcoi1  5575  f1orel  5645  funbrfv  5742  funbrfv2b  5750  fvmptss2  5783  mptrcl  5791  elfvmptrab1  5804  funfvbrb  5825  fmptco  5877  funopsn  5894  funresdfunsnss  5921  elmpocl  6287  relmptopab  6294  funexw  6345  elmpom  6478  mpoxopn0yelv  6515  tfrlem6  6592  funresdfunsndc  6784  pmresg  6962  fundmen  7100  caseinl  7437  caseinr  7438  axaddf  8241  axmulf  8242  hashinfom  11238  4sqlemffi  13203  structcnvcnv  13425  mgpplusg  14328  lidlmex  14920  mplbas  15223  istopon  15256  eltg4i  15298  eltg3  15300  tg1  15302  tg2  15303  tgclb  15308  lmrcl  15435  1vgrex  16483  edg0iedg0g  16529  umgrnloopv  16577  edg0usgr  16710