Theorem funrel 5234

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

Syntax hints:   → wi 4   ⊆ wss 3130   I cid 4289  ^◡ccnv 4626   ∘ ccom 4631  Rel wrel 4632  Fun wfun 5211

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 5219

This theorem is referenced by:  0nelfun  5235  funeu  5242  nfunv  5250  funopg  5251  funssres  5259  funun  5261  fununi  5285  funcnvres2  5292  funimaexg  5301  fnrel  5315  fcoi1  5397  f1orel  5465  funbrfv  5555  funbrfv2b  5561  fvmptss2  5592  mptrcl  5599  elfvmptrab1  5611  funfvbrb  5630  fmptco  5683  funresdfunsnss  5720  elmpocl  6069  funexw  6113  mpoxopn0yelv  6240  tfrlem6  6317  funresdfunsndc  6507  pmresg  6676  fundmen  6806  caseinl  7090  caseinr  7091  axaddf  7867  axmulf  7868  hashinfom  10758  structcnvcnv  12478  istopon  13516  eltg4i  13558  eltg3  13560  tg1  13562  tg2  13563  tgclb  13568  lmrcl  13694