Theorem funrel 5335

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

Syntax hints:   → wi 4   ⊆ wss 3197   I cid 4379  ^◡ccnv 4718   ∘ ccom 4723  Rel wrel 4724  Fun wfun 5312

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 5320

This theorem is referenced by:  0nelfun  5336  funeu  5343  nfunv  5351  funopg  5352  funssres  5360  funun  5362  fununfun  5364  fununi  5389  funcnvres2  5396  funimaexg  5405  fnrel  5419  fcoi1  5508  f1orel  5577  funbrfv  5672  funbrfv2b  5680  fvmptss2  5711  mptrcl  5719  elfvmptrab1  5731  funfvbrb  5750  fmptco  5803  funopsn  5819  funresdfunsnss  5846  elmpocl  6206  relmptopab  6213  funexw  6263  mpoxopn0yelv  6391  tfrlem6  6468  funresdfunsndc  6660  pmresg  6831  fundmen  6967  caseinl  7266  caseinr  7267  axaddf  8063  axmulf  8064  hashinfom  11008  4sqlemffi  12927  structcnvcnv  13056  lidlmex  14447  istopon  14695  eltg4i  14737  eltg3  14739  tg1  14741  tg2  14742  tgclb  14747  lmrcl  14874  1vgrex  15829  edg0iedg0g  15874  umgrnloopv  15922