Theorem funrel 5394

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3220   I cid 4433  ^◡ccnv 4773   ∘ ccom 4778  Rel wrel 4779  Fun wfun 5371

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-fun 5379

This theorem is used by:  0nelfun  5395  funeu  5402  nfunv  5410  funopg  5411  funssres  5420  funun  5422  fununfun  5424  fununi  5449  funcnvres2  5456  funimaexg  5465  fnrel  5479  fcoi1  5572  f1orel  5642  funbrfv  5739  funbrfv2b  5747  fvmptss2  5780  mptrcl  5788  elfvmptrab1  5801  funfvbrb  5822  fmptco  5874  funopsn  5891  funresdfunsnss  5918  elmpocl  6284  relmptopab  6291  funexw  6341  elmpom  6474  mpoxopn0yelv  6510  tfrlem6  6587  funresdfunsndc  6779  pmresg  6957  fundmen  7094  caseinl  7431  caseinr  7432  axaddf  8235  axmulf  8236  hashinfom  11219  4sqlemffi  13177  structcnvcnv  13370  mgpplusg  14224  lidlmex  14814  istopon  15116  eltg4i  15158  eltg3  15160  tg1  15162  tg2  15163  tgclb  15168  lmrcl  15295  1vgrex  16273  edg0iedg0g  16319  umgrnloopv  16367  edg0usgr  16500