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  6514  tfrlem6  6591  funresdfunsndc  6783  pmresg  6961  fundmen  7098  caseinl  7437  caseinr  7438  axaddf  8241  axmulf  8242  hashinfom  11239  4sqlemffi  13204  structcnvcnv  13426  mgpplusg  14329  lidlmex  14921  istopon  15239  eltg4i  15281  eltg3  15283  tg1  15285  tg2  15286  tgclb  15291  lmrcl  15418  1vgrex  16466  edg0iedg0g  16512  umgrnloopv  16560  edg0usgr  16693