Theorem funrel 5215

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

Syntax hints:   → wi 4   ⊆ wss 3121   I cid 4273  ^◡ccnv 4610   ∘ ccom 4615  Rel wrel 4616  Fun wfun 5192

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 5200

This theorem is referenced by:  0nelfun  5216  funeu  5223  nfunv  5231  funopg  5232  funssres  5240  funun  5242  fununi  5266  funcnvres2  5273  funimaexg  5282  fnrel  5296  fcoi1  5378  f1orel  5445  funbrfv  5535  funbrfv2b  5541  fvmptss2  5571  mptrcl  5578  elfvmptrab1  5590  funfvbrb  5609  fmptco  5662  funresdfunsnss  5699  elmpocl  6047  funexw  6091  mpoxopn0yelv  6218  tfrlem6  6295  funresdfunsndc  6485  pmresg  6654  fundmen  6784  caseinl  7068  caseinr  7069  axaddf  7830  axmulf  7831  hashinfom  10712  structcnvcnv  12432  istopon  12805  eltg4i  12849  eltg3  12851  tg1  12853  tg2  12854  tgclb  12859  lmrcl  12985