Theorem funrel 5374

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

Syntax hints:   → wi 4   ⊆ wss 3214   I cid 4414  ^◡ccnv 4753   ∘ ccom 4758  Rel wrel 4759  Fun wfun 5351

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 5359

This theorem is referenced by:  0nelfun  5375  funeu  5382  nfunv  5390  funopg  5391  funssres  5400  funun  5402  fununfun  5404  fununi  5429  funcnvres2  5436  funimaexg  5445  fnrel  5459  fcoi1  5552  f1orel  5622  funbrfv  5718  funbrfv2b  5726  fvmptss2  5757  mptrcl  5765  elfvmptrab1  5777  funfvbrb  5796  fmptco  5848  funopsn  5865  funresdfunsnss  5892  elmpocl  6257  relmptopab  6264  funexw  6314  elmpom  6447  mpoxopn0yelv  6483  tfrlem6  6560  funresdfunsndc  6752  pmresg  6923  fundmen  7060  caseinl  7395  caseinr  7396  axaddf  8199  axmulf  8200  hashinfom  11169  4sqlemffi  13122  structcnvcnv  13315  lidlmex  14752  istopon  15007  eltg4i  15049  eltg3  15051  tg1  15053  tg2  15054  tgclb  15059  lmrcl  15186  1vgrex  16144  edg0iedg0g  16190  umgrnloopv  16238  edg0usgr  16371