Theorem funrel 6242

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

Syntax hints:   → wi 4   ⊆ wss 3859   I cid 5347  ^◡ccnv 5442   ∘ ccom 5447  Rel wrel 5448  Fun wfun 6219

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 208  df-an 397  df-fun 6227

This theorem is referenced by:  0nelfun  6243  funeu  6250  nfunv  6258  funopg  6259  funssres  6268  funun  6270  fununfun  6272  fununi  6299  funcnvres2  6304  fnrel  6324  fcoi1  6420  f1orel  6486  funbrfv  6584  funbrfv2b  6591  funfv2  6618  funfvbrb  6686  fimacnvinrn  6705  fvn0ssdmfun  6707  funopsn  6773  funresdfunsn  6818  funexw  7509  funfv1st2nd  7601  funelss  7602  funeldmdif  7603  wfrrel  7812  tfrlem6  7870  tfr2b  7884  pmresg  8284  fundmen  8431  resfifsupp  8707  rankwflemb  9068  gruima  10070  structcnvcnv  16326  inviso1  16865  setciso  17180  edg0iedg0  26523  edg0usgr  26718  usgr1v0edg  26722  fgreu  30107  cycpmconjvlem  30420  cycpmconjslem2  30435  bnj1379  31719  funen1cnv  31971  fundmpss  32617  funsseq  32619  frrlem6  32737  nolt02o  32808  nosupbnd1  32823  nosupbnd2lem1  32824  nosupbnd2  32825  noetalem2  32827  noetalem3  32828  imageval  33000  imagesset  33023  cocnv  34532  frege124d  39591  frege129d  39593  frege133d  39595  funbrafv  42873  funbrafv2b  42874  funbrafv2  42962  rngciso  43731  rngcisoALTV  43743  ringciso  43782  ringcisoALTV  43806