Theorem funrel 6548

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899   I cid 5545  ^◡ccnv 5650   ∘ ccom 5655  Rel wrel 5656  Fun wfun 6525

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fun 6533

This theorem is used by:  0nelfun  6549  funeu  6557  nfunv  6565  funopg  6566  funssres  6576  funun  6578  fununfun  6580  fununi  6607  funcnvres2  6612  fnrel  6633  fcoi1  6748  f1orel  6819  funbrfv  6925  funbrfv2b  6934  funfv2  6965  funfvbrb  7042  fimacnvinrn  7063  fvn0ssdmfun  7066  funopsnOLD  7144  funexw  7953  funfv1st2nd  8046  funelss  8047  funeldmdif  8048  frrlem6  8293  tfrlem6OLD  8374  tfr2b  8388  pmresg  8882  funen1cnv  9040  fundmen  9043  rankwflemb  9783  gruima  10868  structcnvcnv  17311  inviso1  17921  setciso  18246  rngciso  20870  ringciso  20904  nolt02o  28034  nogt01o  28035  nosupbnd1  28053  nosupbnd2lem1  28054  nosupbnd2  28055  noinfbnd1  28068  noinfbnd2lem1  28069  noinfbnd2  28070  noetasuplem2  28073  noetasuplem3  28074  noetasuplem4  28075  noetainflem2  28077  edg0iedg0  29615  edg0usgr  29816  usgr1v0edg  29820  fgreu  33247  fressupp  33263  gsumhashmul  33610  cycpmconjvlem  33684  cycpmconjslem2  33698  bnj1379  35443  fundmpss  36501  funsseq  36502  imageval  36662  imagesset  36687  cocnv  38627  frege124d  44720  frege129d  44722  frege133d  44724  funbrafv  48172  funbrafv2b  48173  funbrafv2  48261  isubgrvtxuhgr  48906  rngcisoALTV  49318  ringcisoALTV  49352  ackvalsuc0val  49743