Theorem funrel 5148

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

Syntax hints:   → wi 4   ⊆ wss 3076   I cid 4218  ^◡ccnv 4546   ∘ ccom 4551  Rel wrel 4552  Fun wfun 5125

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

This theorem depends on definitions:  df-bi 116  df-fun 5133

This theorem is referenced by:  0nelfun  5149  funeu  5156  nfunv  5164  funopg  5165  funssres  5173  funun  5175  fununi  5199  funcnvres2  5206  funimaexg  5215  fnrel  5229  fcoi1  5311  f1orel  5378  funbrfv  5468  funbrfv2b  5474  fvmptss2  5504  mptrcl  5511  elfvmptrab1  5523  funfvbrb  5541  fmptco  5594  funresdfunsnss  5631  elmpocl  5976  mpoxopn0yelv  6144  tfrlem6  6221  funresdfunsndc  6410  pmresg  6578  fundmen  6708  caseinl  6984  caseinr  6985  axaddf  7700  axmulf  7701  hashinfom  10556  structcnvcnv  12014  istopon  12219  eltg4i  12263  eltg3  12265  tg1  12267  tg2  12268  tgclb  12273  lmrcl  12399