Theorem funrel 5271

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

Syntax hints:   → wi 4   ⊆ wss 3153   I cid 4319  ^◡ccnv 4658   ∘ ccom 4663  Rel wrel 4664  Fun wfun 5248

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 5256

This theorem is referenced by:  0nelfun  5272  funeu  5279  nfunv  5287  funopg  5288  funssres  5296  funun  5298  fununi  5322  funcnvres2  5329  funimaexg  5338  fnrel  5352  fcoi1  5434  f1orel  5503  funbrfv  5595  funbrfv2b  5601  fvmptss2  5632  mptrcl  5640  elfvmptrab1  5652  funfvbrb  5671  fmptco  5724  funresdfunsnss  5761  elmpocl  6113  funexw  6164  mpoxopn0yelv  6292  tfrlem6  6369  funresdfunsndc  6559  pmresg  6730  fundmen  6860  caseinl  7150  caseinr  7151  axaddf  7928  axmulf  7929  hashinfom  10849  4sqlemffi  12534  structcnvcnv  12634  lidlmex  13971  istopon  14181  eltg4i  14223  eltg3  14225  tg1  14227  tg2  14228  tgclb  14233  lmrcl  14359