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  11041  4sqlemffi  12971  structcnvcnv  13100  lidlmex  14492  istopon  14740  eltg4i  14782  eltg3  14784  tg1  14786  tg2  14787  tgclb  14792  lmrcl  14919  1vgrex  15874  edg0iedg0g  15920  umgrnloopv  15968  edg0usgr  16101