Theorem funrel 6533

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

Syntax hints:   → wi 4   ⊆ wss 3914   I cid 5532  ^◡ccnv 5637   ∘ ccom 5642  Rel wrel 5643  Fun wfun 6505

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 6513

This theorem is referenced by:  0nelfun  6534  funeu  6541  nfunv  6549  funopg  6550  funssres  6560  funun  6562  fununfun  6564  fununi  6591  funcnvres2  6596  fnrel  6620  fcoi1  6734  f1orel  6803  funbrfv  6909  funbrfv2b  6918  funfv2  6949  funfvbrb  7023  fimacnvinrn  7043  fvn0ssdmfun  7046  funopsn  7120  funresdfunsn  7163  funexw  7930  funfv1st2nd  8025  funelss  8026  funeldmdif  8027  frrlem6  8270  tfrlem6  8350  tfr2b  8364  pmresg  8843  fundmen  9002  resfifsupp  9348  rankwflemb  9746  gruima  10755  structcnvcnv  17123  inviso1  17728  setciso  18053  rngciso  20547  ringciso  20581  nolt02o  27607  nogt01o  27608  nosupbnd1  27626  nosupbnd2lem1  27627  nosupbnd2  27628  noinfbnd1  27641  noinfbnd2lem1  27642  noinfbnd2  27643  noetasuplem2  27646  noetasuplem3  27647  noetasuplem4  27648  noetainflem2  27650  edg0iedg0  28982  edg0usgr  29180  usgr1v0edg  29184  fgreu  32596  fressupp  32611  gsumhashmul  33001  cycpmconjvlem  33098  cycpmconjslem2  33112  bnj1379  34820  funen1cnv  35078  fundmpss  35754  funsseq  35755  imageval  35918  imagesset  35941  cocnv  37719  frege124d  43750  frege129d  43752  frege133d  43754  funbrafv  47159  funbrafv2b  47160  funbrafv2  47248  isubgrvtxuhgr  47864  rngcisoALTV  48265  ringcisoALTV  48299  ackvalsuc0val  48676