Theorem funrel 6371

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

Syntax hints:   → wi 4   ⊆ wss 3935   I cid 5458  ^◡ccnv 5553   ∘ ccom 5558  Rel wrel 5559  Fun wfun 6348

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 209  df-an 399  df-fun 6356

This theorem is referenced by:  0nelfun  6372  funeu  6379  nfunv  6387  funopg  6388  funssres  6397  funun  6399  fununfun  6401  fununi  6428  funcnvres2  6433  fnrel  6453  fcoi1  6551  f1orel  6617  funbrfv  6715  funbrfv2b  6722  funfv2  6750  funfvbrb  6820  fimacnvinrn  6839  fvn0ssdmfun  6841  funopsn  6909  funresdfunsn  6950  funexw  7652  funfv1st2nd  7744  funelss  7745  funeldmdif  7746  wfrrel  7959  tfrlem6  8017  tfr2b  8031  pmresg  8433  fundmen  8582  resfifsupp  8860  rankwflemb  9221  gruima  10223  structcnvcnv  16496  inviso1  17035  setciso  17350  edg0iedg0  26839  edg0usgr  27034  usgr1v0edg  27038  fgreu  30416  cycpmconjvlem  30783  cycpmconjslem2  30797  bnj1379  32102  funen1cnv  32357  fundmpss  33009  funsseq  33011  frrlem6  33128  nolt02o  33199  nosupbnd1  33214  nosupbnd2lem1  33215  nosupbnd2  33216  noetalem2  33218  noetalem3  33219  imageval  33391  imagesset  33414  cocnv  34999  frege124d  40104  frege129d  40106  frege133d  40108  funbrafv  43356  funbrafv2b  43357  funbrafv2  43445  rngciso  44252  rngcisoALTV  44264  ringciso  44303  ringcisoALTV  44327