Theorem funrel 6595

Description: A function is a relation. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
funrel	⊢ (Fun 𝐴 → Rel 𝐴)

Proof of Theorem funrel

Step	Hyp	Ref	Expression
1		df-fun 6575	. 2 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ))
2	1	simplbi 497	1 ⊢ (Fun 𝐴 → Rel 𝐴)

Syntax hints:   → wi 4   ⊆ wss 3976   I cid 5592  ^◡ccnv 5699   ∘ ccom 5704  Rel wrel 5705  Fun wfun 6567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-fun 6575

This theorem is referenced by:  0nelfun  6596  funeu  6603  nfunv  6611  funopg  6612  funssres  6622  funun  6624  fununfun  6626  fununi  6653  funcnvres2  6658  fnrel  6681  fcoi1  6795  f1orel  6865  funbrfv  6971  funbrfv2b  6979  funfv2  7010  funfvbrb  7084  fimacnvinrn  7105  fvn0ssdmfun  7108  funopsn  7182  funresdfunsn  7223  funexw  7992  funfv1st2nd  8087  funelss  8088  funeldmdif  8089  frrlem6  8332  wfrrelOLD  8370  tfrlem6  8438  tfr2b  8452  pmresg  8928  fundmen  9096  resfifsupp  9466  rankwflemb  9862  gruima  10871  structcnvcnv  17200  inviso1  17827  setciso  18158  rngciso  20660  ringciso  20694  nolt02o  27758  nogt01o  27759  nosupbnd1  27777  nosupbnd2lem1  27778  nosupbnd2  27779  noinfbnd1  27792  noinfbnd2lem1  27793  noinfbnd2  27794  noetasuplem2  27797  noetasuplem3  27798  noetasuplem4  27799  noetainflem2  27801  edg0iedg0  29090  edg0usgr  29288  usgr1v0edg  29292  fgreu  32690  fressupp  32700  gsumhashmul  33040  cycpmconjvlem  33134  cycpmconjslem2  33148  bnj1379  34806  funen1cnv  35064  fundmpss  35730  funsseq  35731  imageval  35894  imagesset  35917  cocnv  37685  frege124d  43723  frege129d  43725  frege133d  43727  funbrafv  47073  funbrafv2b  47074  funbrafv2  47162  isubgrvtxuhgr  47736  rngcisoALTV  48000  ringcisoALTV  48034  ackvalsuc0val  48421