Theorem funrel 6542

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

Syntax hints:   → wi 4   ⊆ wss 3907   I cid 5546  ^◡ccnv 5651   ∘ ccom 5656  Rel wrel 5657  Fun wfun 6519

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 210  df-an 401  df-fun 6527

This theorem is referenced by:  0nelfun  6543  funeu  6550  nfunv  6558  funopg  6559  funssres  6569  funun  6571  fununfun  6573  fununi  6600  funcnvres2  6605  fnrel  6627  fcoi1  6742  f1orel  6813  funbrfv  6919  funbrfv2b  6928  funfv2  6959  funfvbrb  7036  fimacnvinrn  7056  fvn0ssdmfun  7059  funopsnOLD  7135  funexw  7937  funfv1st2nd  8031  funelss  8032  funeldmdif  8033  frrlem6  8276  tfrlem6OLD  8357  tfr2b  8371  pmresg  8856  fundmen  9016  rankwflemb  9753  gruima  10775  structcnvcnv  17203  inviso1  17813  setciso  18138  rngciso  20714  ringciso  20748  nolt02o  27817  nogt01o  27818  nosupbnd1  27836  nosupbnd2lem1  27837  nosupbnd2  27838  noinfbnd1  27851  noinfbnd2lem1  27852  noinfbnd2  27853  noetasuplem2  27856  noetasuplem3  27857  noetasuplem4  27858  noetainflem2  27860  edg0iedg0  29314  edg0usgr  29512  usgr1v0edg  29516  fgreu  32928  fressupp  32945  gsumhashmul  33300  cycpmconjvlem  33374  cycpmconjslem2  33388  bnj1379  35135  funen1cnv  35392  fundmpss  36130  funsseq  36131  imageval  36291  imagesset  36316  cocnv  38236  frege124d  44349  frege129d  44351  frege133d  44353  funbrafv  47750  funbrafv2b  47751  funbrafv2  47839  isubgrvtxuhgr  48484  rngcisoALTV  48897  ringcisoALTV  48931  ackvalsuc0val  49318