Theorem funrel 5943

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 5928	. 2 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ))
2	1	simplbi 475	1 ⊢ (Fun 𝐴 → Rel 𝐴)

Syntax hints:   → wi 4   ⊆ wss 3607   I cid 5052  ^◡ccnv 5142   ∘ ccom 5147  Rel wrel 5148  Fun wfun 5920

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 197  df-an 385  df-fun 5928

This theorem is referenced by:  0nelfun  5944  funeu  5951  nfunv  5959  funopg  5960  funssres  5968  funun  5970  fununfun  5972  fununi  6002  funcnvres2  6007  fnrel  6027  fcoi1  6116  f1orel  6178  funbrfv  6272  funbrfv2b  6279  funfv2  6305  funfvbrb  6370  fimacnvinrn  6388  fvn0ssdmfun  6390  funopsn  6453  funresdfunsn  6496  wfrrel  7465  tfrlem6  7523  tfr2b  7537  pmresg  7927  fundmen  8071  resfifsupp  8344  rankwflemb  8694  gruima  9662  structcnvcnv  15918  inviso1  16473  setciso  16788  pmtrsn  17985  00lsp  19029  edg0iedg0  25994  edg0iedg0OLD  25995  edg0usgr  26190  usgr1v0edg  26194  fmptcof2  29585  fgreu  29599  bnj1379  31027  fundmpss  31790  funsseq  31792  frrlem5b  31910  frrlem6  31914  nolt02o  31970  nosupbnd1  31985  nosupbnd2lem1  31986  nosupbnd2  31987  noetalem2  31989  noetalem3  31990  imageval  32162  imagesset  32185  cocnv  33650  frege124d  38370  frege129d  38372  frege133d  38374  funbrafv  41559  funbrafv2b  41560  rngciso  42307  rngcisoALTV  42319  ringciso  42358  ringcisoALTV  42382