Theorem funrel 5272

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 5257	. 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 3154   _I cid 4320   `'ccnv 4659   o. ccom 4664   Rel wrel 4665   Fun wfun 5249

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 5257

This theorem is referenced by:  0nelfun  5273  funeu  5280  nfunv  5288  funopg  5289  funssres  5297  funun  5299  fununi  5323  funcnvres2  5330  funimaexg  5339  fnrel  5353  fcoi1  5435  f1orel  5504  funbrfv  5596  funbrfv2b  5602  fvmptss2  5633  mptrcl  5641  elfvmptrab1  5653  funfvbrb  5672  fmptco  5725  funresdfunsnss  5762  elmpocl  6115  funexw  6166  mpoxopn0yelv  6294  tfrlem6  6371  funresdfunsndc  6561  pmresg  6732  fundmen  6862  caseinl  7152  caseinr  7153  axaddf  7930  axmulf  7931  hashinfom  10852  4sqlemffi  12537  structcnvcnv  12637  lidlmex  13974  istopon  14192  eltg4i  14234  eltg3  14236  tg1  14238  tg2  14239  tgclb  14244  lmrcl  14370