Theorem funrel 5394

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 5379	. 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 4433   `'ccnv 4773   o. ccom 4778   Rel wrel 4779   Fun wfun 5371

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 5379

This theorem is used by:  0nelfun  5395  funeu  5402  nfunv  5410  funopg  5411  funssres  5420  funun  5422  fununfun  5424  fununi  5449  funcnvres2  5456  funimaexg  5465  fnrel  5479  fcoi1  5572  f1orel  5642  funbrfv  5739  funbrfv2b  5747  fvmptss2  5780  mptrcl  5788  elfvmptrab1  5801  funfvbrb  5822  fmptco  5874  funopsn  5891  funresdfunsnss  5918  elmpocl  6284  relmptopab  6291  funexw  6341  elmpom  6474  mpoxopn0yelv  6510  tfrlem6  6587  funresdfunsndc  6779  pmresg  6957  fundmen  7094  caseinl  7431  caseinr  7432  axaddf  8235  axmulf  8236  hashinfom  11231  4sqlemffi  13195  structcnvcnv  13417  mgpplusg  14271  lidlmex  14861  istopon  15163  eltg4i  15205  eltg3  15207  tg1  15209  tg2  15210  tgclb  15215  lmrcl  15342  1vgrex  16359  edg0iedg0g  16405  umgrnloopv  16453  edg0usgr  16586