Theorem funrel 5397

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3220   I cid 4435  ^◡ccnv 4775   ∘ ccom 4780  Rel wrel 4781  Fun wfun 5374

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 5382

This theorem is used by:  0nelfun  5398  funeu  5405  nfunv  5413  funopg  5414  funssres  5423  funun  5425  fununfun  5427  fununi  5452  funcnvres2  5459  funimaexg  5468  fnrel  5482  fcoi1  5575  f1orel  5645  funbrfv  5742  funbrfv2b  5750  fvmptss2  5783  mptrcl  5791  elfvmptrab1  5804  funfvbrb  5825  fmptco  5877  funopsn  5894  funresdfunsnss  5921  elmpocl  6287  relmptopab  6294  funexw  6345  elmpom  6478  mpoxopn0yelv  6514  tfrlem6  6591  funresdfunsndc  6783  pmresg  6961  fundmen  7099  caseinl  7438  caseinr  7439  axaddf  8242  axmulf  8243  hashinfom  11240  4sqlemffi  13205  structcnvcnv  13427  mgpplusg  14330  lidlmex  14922  istopon  15251  eltg4i  15293  eltg3  15295  tg1  15297  tg2  15298  tgclb  15303  lmrcl  15430  1vgrex  16478  edg0iedg0g  16524  umgrnloopv  16572  edg0usgr  16705