Theorem funrel 6579

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900   I cid 5550  ^◡ccnv 5655   ∘ ccom 5660  Rel wrel 5661  Fun wfun 6555

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 6563

This theorem is used by:  0nelfun  6580  funeu  6588  nfunv  6596  funopg  6597  funssres  6607  funun  6609  fununfunOLD  6612  fununi  6640  funcnvres2  6645  fnrel  6666  fcoi1  6781  f1orel  6852  funbrfv  6959  funbrfv2b  6968  funfv2  6999  funfvbrb  7076  fimacnvinrn  7098  fvn0ssdmfun  7101  funopsnOLD  7179  funexw  7991  funfv1st2nd  8085  funelss  8086  funeldmdif  8087  frrlem6  8340  tfrlem6OLD  8421  tfr2b  8435  pmresg  8929  funen1cnv  9087  fundmen  9090  rankwflembOLD  9831  gruima  10917  structcnvcnv  17363  inviso1  17973  setciso  18298  rngciso  20923  ringciso  20957  nolt02o  28085  nogt01o  28086  nosupbnd1  28104  nosupbnd2lem1  28105  nosupbnd2  28106  noinfbnd1  28119  noinfbnd2lem1  28120  noinfbnd2  28121  noetasuplem2  28124  noetasuplem3  28125  noetasuplem4  28126  noetainflem2  28128  edg0iedg0  29666  edg0usgr  29867  usgr1v0edg  29871  fgreu  33340  fressupp  33355  gsumhashmul  33704  cycpmconjvlem  33778  cycpmconjslem2  33792  bnj1379  35543  fundmpss  36723  funsseq  36724  imageval  36883  imagesset  36908  cocnv  38864  frege124d  44964  frege129d  44966  frege133d  44968  hfstructcan  46240  funbrafv  48443  funbrafv2b  48444  funbrafv2  48532  isubgrvtxuhgr  49177  rngcisoALTV  49589  ringcisoALTV  49623  ackvalsuc0val  50014