Theorem funrel 6498

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

Syntax hints:   → wi 4   ⊆ wss 3902   I cid 5510  ^◡ccnv 5615   ∘ ccom 5620  Rel wrel 5621  Fun wfun 6475

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 6483

This theorem is referenced by:  0nelfun  6499  funeu  6506  nfunv  6514  funopg  6515  funssres  6525  funun  6527  fununfun  6529  fununi  6556  funcnvres2  6561  fnrel  6583  fcoi1  6697  f1orel  6766  funbrfv  6870  funbrfv2b  6879  funfv2  6910  funfvbrb  6984  fimacnvinrn  7004  fvn0ssdmfun  7007  funopsn  7081  funresdfunsn  7123  funexw  7884  funfv1st2nd  7978  funelss  7979  funeldmdif  7980  frrlem6  8221  tfrlem6  8301  tfr2b  8315  pmresg  8794  fundmen  8953  resfifsupp  9281  rankwflemb  9683  gruima  10690  structcnvcnv  17061  inviso1  17670  setciso  17995  rngciso  20551  ringciso  20585  nolt02o  27632  nogt01o  27633  nosupbnd1  27651  nosupbnd2lem1  27652  nosupbnd2  27653  noinfbnd1  27666  noinfbnd2lem1  27667  noinfbnd2  27668  noetasuplem2  27671  noetasuplem3  27672  noetasuplem4  27673  noetainflem2  27675  edg0iedg0  29031  edg0usgr  29229  usgr1v0edg  29233  fgreu  32649  fressupp  32664  gsumhashmul  33036  cycpmconjvlem  33105  cycpmconjslem2  33119  bnj1379  34837  funen1cnv  35095  fundmpss  35799  funsseq  35800  imageval  35963  imagesset  35986  cocnv  37764  frege124d  43793  frege129d  43795  frege133d  43797  funbrafv  47188  funbrafv2b  47189  funbrafv2  47277  isubgrvtxuhgr  47894  rngcisoALTV  48307  ringcisoALTV  48341  ackvalsuc0val  48718