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  7432  caseinr  7433  axaddf  8236  axmulf  8237  hashinfom  11233  4sqlemffi  13198  structcnvcnv  13420  mgpplusg  14306  lidlmex  14896  istopon  15205  eltg4i  15247  eltg3  15249  tg1  15251  tg2  15252  tgclb  15257  lmrcl  15384  1vgrex  16427  edg0iedg0g  16473  umgrnloopv  16521  edg0usgr  16654