Theorem funrel 5341

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

Syntax hints:   → wi 4   ⊆ wss 3198   I cid 4383  ^◡ccnv 4722   ∘ ccom 4727  Rel wrel 4728  Fun wfun 5318

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 5326

This theorem is referenced by:  0nelfun  5342  funeu  5349  nfunv  5357  funopg  5358  funssres  5366  funun  5368  fununfun  5370  fununi  5395  funcnvres2  5402  funimaexg  5411  fnrel  5425  fcoi1  5514  f1orel  5583  funbrfv  5678  funbrfv2b  5686  fvmptss2  5717  mptrcl  5725  elfvmptrab1  5737  funfvbrb  5756  fmptco  5809  funopsn  5825  funresdfunsnss  5852  elmpocl  6212  relmptopab  6219  funexw  6269  elmpom  6398  mpoxopn0yelv  6400  tfrlem6  6477  funresdfunsndc  6669  pmresg  6840  fundmen  6976  caseinl  7284  caseinr  7285  axaddf  8081  axmulf  8082  hashinfom  11033  4sqlemffi  12962  structcnvcnv  13091  lidlmex  14482  istopon  14730  eltg4i  14772  eltg3  14774  tg1  14776  tg2  14777  tgclb  14782  lmrcl  14909  1vgrex  15864  edg0iedg0g  15910  umgrnloopv  15958  edg0usgr  16091