Theorem funrel 5276

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

Syntax hints:   → wi 4   ⊆ wss 3157   I cid 4324  ^◡ccnv 4663   ∘ ccom 4668  Rel wrel 4669  Fun wfun 5253

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 5261

This theorem is referenced by:  0nelfun  5277  funeu  5284  nfunv  5292  funopg  5293  funssres  5301  funun  5303  fununi  5327  funcnvres2  5334  funimaexg  5343  fnrel  5357  fcoi1  5439  f1orel  5508  funbrfv  5600  funbrfv2b  5606  fvmptss2  5637  mptrcl  5645  elfvmptrab1  5657  funfvbrb  5676  fmptco  5729  funresdfunsnss  5766  elmpocl  6119  funexw  6170  mpoxopn0yelv  6298  tfrlem6  6375  funresdfunsndc  6565  pmresg  6736  fundmen  6866  caseinl  7158  caseinr  7159  axaddf  7937  axmulf  7938  hashinfom  10872  4sqlemffi  12575  structcnvcnv  12704  lidlmex  14041  istopon  14259  eltg4i  14301  eltg3  14303  tg1  14305  tg2  14306  tgclb  14311  lmrcl  14437