Theorem funrel 5371

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

Syntax hints:   → wi 4   ⊆ wss 3213   I cid 4411  ^◡ccnv 4750   ∘ ccom 4755  Rel wrel 4756  Fun wfun 5348

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 5356

This theorem is referenced by:  0nelfun  5372  funeu  5379  nfunv  5387  funopg  5388  funssres  5397  funun  5399  fununfun  5401  fununi  5426  funcnvres2  5433  funimaexg  5442  fnrel  5456  fcoi1  5549  f1orel  5619  funbrfv  5715  funbrfv2b  5723  fvmptss2  5754  mptrcl  5762  elfvmptrab1  5774  funfvbrb  5793  fmptco  5845  funopsn  5862  funresdfunsnss  5889  elmpocl  6251  relmptopab  6258  funexw  6307  elmpom  6436  mpoxopn0yelv  6472  tfrlem6  6549  funresdfunsndc  6741  pmresg  6912  fundmen  7049  caseinl  7384  caseinr  7385  axaddf  8188  axmulf  8189  hashinfom  11149  4sqlemffi  13102  structcnvcnv  13249  lidlmex  14672  istopon  14927  eltg4i  14969  eltg3  14971  tg1  14973  tg2  14974  tgclb  14979  lmrcl  15106  1vgrex  16064  edg0iedg0g  16110  umgrnloopv  16158  edg0usgr  16291