Theorem funrel 5235

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

Syntax hints:   → wi 4   ⊆ wss 3131   I cid 4290  ^◡ccnv 4627   ∘ ccom 4632  Rel wrel 4633  Fun wfun 5212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-fun 5220

This theorem is referenced by:  0nelfun  5236  funeu  5243  nfunv  5251  funopg  5252  funssres  5260  funun  5262  fununi  5286  funcnvres2  5293  funimaexg  5302  fnrel  5316  fcoi1  5398  f1orel  5466  funbrfv  5556  funbrfv2b  5562  fvmptss2  5593  mptrcl  5600  elfvmptrab1  5612  funfvbrb  5631  fmptco  5684  funresdfunsnss  5721  elmpocl  6071  funexw  6115  mpoxopn0yelv  6242  tfrlem6  6319  funresdfunsndc  6509  pmresg  6678  fundmen  6808  caseinl  7092  caseinr  7093  axaddf  7869  axmulf  7870  hashinfom  10760  structcnvcnv  12480  istopon  13598  eltg4i  13640  eltg3  13642  tg1  13644  tg2  13645  tgclb  13650  lmrcl  13776