Theorem funrel 5343

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

Syntax hints:   → wi 4   ⊆ wss 3200   I cid 4385  ^◡ccnv 4724   ∘ ccom 4729  Rel wrel 4730  Fun wfun 5320

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 5328

This theorem is referenced by:  0nelfun  5344  funeu  5351  nfunv  5359  funopg  5360  funssres  5369  funun  5371  fununfun  5373  fununi  5398  funcnvres2  5405  funimaexg  5414  fnrel  5428  fcoi1  5517  f1orel  5586  funbrfv  5682  funbrfv2b  5690  fvmptss2  5721  mptrcl  5729  elfvmptrab1  5741  funfvbrb  5760  fmptco  5813  funopsn  5830  funresdfunsnss  5857  elmpocl  6217  relmptopab  6224  funexw  6274  elmpom  6403  mpoxopn0yelv  6405  tfrlem6  6482  funresdfunsndc  6674  pmresg  6845  fundmen  6981  caseinl  7290  caseinr  7291  axaddf  8088  axmulf  8089  hashinfom  11040  4sqlemffi  12970  structcnvcnv  13099  lidlmex  14491  istopon  14739  eltg4i  14781  eltg3  14783  tg1  14785  tg2  14786  tgclb  14791  lmrcl  14918  1vgrex  15873  edg0iedg0g  15919  umgrnloopv  15967  edg0usgr  16100