Theorem funrel 5293

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

Syntax hints:   → wi 4   ⊆ wss 3167   I cid 4339  ^◡ccnv 4678   ∘ ccom 4683  Rel wrel 4684  Fun wfun 5270

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 5278

This theorem is referenced by:  0nelfun  5294  funeu  5301  nfunv  5309  funopg  5310  funssres  5318  funun  5320  fununfun  5322  fununi  5347  funcnvres2  5354  funimaexg  5363  fnrel  5377  fcoi1  5463  f1orel  5532  funbrfv  5624  funbrfv2b  5630  fvmptss2  5661  mptrcl  5669  elfvmptrab1  5681  funfvbrb  5700  fmptco  5753  funopsn  5769  funresdfunsnss  5794  elmpocl  6148  funexw  6204  mpoxopn0yelv  6332  tfrlem6  6409  funresdfunsndc  6599  pmresg  6770  fundmen  6905  caseinl  7200  caseinr  7201  axaddf  7988  axmulf  7989  hashinfom  10930  4sqlemffi  12763  structcnvcnv  12892  lidlmex  14281  istopon  14529  eltg4i  14571  eltg3  14573  tg1  14575  tg2  14576  tgclb  14581  lmrcl  14707  1vgrex  15663  edg0iedg0g  15706