Theorem funrel 5345

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

Syntax hints:   → wi 4   ⊆ wss 3199   I cid 4387  ^◡ccnv 4726   ∘ ccom 4731  Rel wrel 4732  Fun wfun 5322

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 5330

This theorem is referenced by:  0nelfun  5346  funeu  5353  nfunv  5361  funopg  5362  funssres  5371  funun  5373  fununfun  5375  fununi  5400  funcnvres2  5407  funimaexg  5416  fnrel  5430  fcoi1  5519  f1orel  5589  funbrfv  5685  funbrfv2b  5693  fvmptss2  5724  mptrcl  5732  elfvmptrab1  5744  funfvbrb  5763  fmptco  5816  funopsn  5833  funresdfunsnss  5860  elmpocl  6222  relmptopab  6229  funexw  6279  elmpom  6408  mpoxopn0yelv  6410  tfrlem6  6487  funresdfunsndc  6679  pmresg  6850  fundmen  6986  caseinl  7295  caseinr  7296  axaddf  8093  axmulf  8094  hashinfom  11046  4sqlemffi  12992  structcnvcnv  13121  lidlmex  14513  istopon  14766  eltg4i  14808  eltg3  14810  tg1  14812  tg2  14813  tgclb  14818  lmrcl  14945  1vgrex  15900  edg0iedg0g  15946  umgrnloopv  15994  edg0usgr  16127