Theorem funrel 6536

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

Syntax hints:   → wi 4   ⊆ wss 3917   I cid 5535  ^◡ccnv 5640   ∘ ccom 5645  Rel wrel 5646  Fun wfun 6508

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 6516

This theorem is referenced by:  0nelfun  6537  funeu  6544  nfunv  6552  funopg  6553  funssres  6563  funun  6565  fununfun  6567  fununi  6594  funcnvres2  6599  fnrel  6623  fcoi1  6737  f1orel  6806  funbrfv  6912  funbrfv2b  6921  funfv2  6952  funfvbrb  7026  fimacnvinrn  7046  fvn0ssdmfun  7049  funopsn  7123  funresdfunsn  7166  funexw  7933  funfv1st2nd  8028  funelss  8029  funeldmdif  8030  frrlem6  8273  tfrlem6  8353  tfr2b  8367  pmresg  8846  fundmen  9005  resfifsupp  9355  rankwflemb  9753  gruima  10762  structcnvcnv  17130  inviso1  17735  setciso  18060  rngciso  20554  ringciso  20588  nolt02o  27614  nogt01o  27615  nosupbnd1  27633  nosupbnd2lem1  27634  nosupbnd2  27635  noinfbnd1  27648  noinfbnd2lem1  27649  noinfbnd2  27650  noetasuplem2  27653  noetasuplem3  27654  noetasuplem4  27655  noetainflem2  27657  edg0iedg0  28989  edg0usgr  29187  usgr1v0edg  29191  fgreu  32603  fressupp  32618  gsumhashmul  33008  cycpmconjvlem  33105  cycpmconjslem2  33119  bnj1379  34827  funen1cnv  35085  fundmpss  35761  funsseq  35762  imageval  35925  imagesset  35948  cocnv  37726  frege124d  43757  frege129d  43759  frege133d  43761  funbrafv  47163  funbrafv2b  47164  funbrafv2  47252  isubgrvtxuhgr  47868  rngcisoALTV  48269  ringcisoALTV  48303  ackvalsuc0val  48680