Theorem funrel 5140

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

Syntax hints:   → wi 4   ⊆ wss 3071   I cid 4210  ^◡ccnv 4538   ∘ ccom 4543  Rel wrel 4544  Fun wfun 5117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-fun 5125

This theorem is referenced by:  0nelfun  5141  funeu  5148  nfunv  5156  funopg  5157  funssres  5165  funun  5167  fununi  5191  funcnvres2  5198  funimaexg  5207  fnrel  5221  fcoi1  5303  f1orel  5370  funbrfv  5460  funbrfv2b  5466  fvmptss2  5496  mptrcl  5503  elfvmptrab1  5515  funfvbrb  5533  fmptco  5586  funresdfunsnss  5623  elmpocl  5968  mpoxopn0yelv  6136  tfrlem6  6213  funresdfunsndc  6402  pmresg  6570  fundmen  6700  caseinl  6976  caseinr  6977  axaddf  7676  axmulf  7677  hashinfom  10524  structcnvcnv  11975  istopon  12180  eltg4i  12224  eltg3  12226  tg1  12228  tg2  12229  tgclb  12234  lmrcl  12360