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  11217  4sqlemffi  13175  structcnvcnv  13368  mgpplusg  14222  lidlmex  14812  istopon  15114  eltg4i  15156  eltg3  15158  tg1  15160  tg2  15161  tgclb  15166  lmrcl  15293  1vgrex  16261  edg0iedg0g  16307  umgrnloopv  16355  edg0usgr  16488