Theorem funrel 5392

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

Syntax hints:   → wi 4   ⊆ wss 3220   I cid 4431  ^◡ccnv 4771   ∘ ccom 4776  Rel wrel 4777  Fun wfun 5369

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 5377

This theorem is referenced by:  0nelfun  5393  funeu  5400  nfunv  5408  funopg  5409  funssres  5418  funun  5420  fununfun  5422  fununi  5447  funcnvres2  5454  funimaexg  5463  fnrel  5477  fcoi1  5570  f1orel  5640  funbrfv  5736  funbrfv2b  5744  fvmptss2  5777  mptrcl  5785  elfvmptrab1  5797  funfvbrb  5816  fmptco  5868  funopsn  5885  funresdfunsnss  5912  elmpocl  6278  relmptopab  6285  funexw  6335  elmpom  6468  mpoxopn0yelv  6504  tfrlem6  6581  funresdfunsndc  6773  pmresg  6951  fundmen  7088  caseinl  7425  caseinr  7426  axaddf  8229  axmulf  8230  hashinfom  11200  4sqlemffi  13158  structcnvcnv  13351  mgpplusg  14205  lidlmex  14795  istopon  15097  eltg4i  15139  eltg3  15141  tg1  15143  tg2  15144  tgclb  15149  lmrcl  15276  1vgrex  16244  edg0iedg0g  16290  umgrnloopv  16338  edg0usgr  16471