Theorem funrel 5368

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

Syntax hints:   → wi 4   ⊆ wss 3210   I cid 4408  ^◡ccnv 4747   ∘ ccom 4752  Rel wrel 4753  Fun wfun 5345

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 5353

This theorem is referenced by:  0nelfun  5369  funeu  5376  nfunv  5384  funopg  5385  funssres  5394  funun  5396  fununfun  5398  fununi  5423  funcnvres2  5430  funimaexg  5439  fnrel  5453  fcoi1  5546  f1orel  5616  funbrfv  5712  funbrfv2b  5720  fvmptss2  5751  mptrcl  5759  elfvmptrab1  5771  funfvbrb  5790  fmptco  5842  funopsn  5859  funresdfunsnss  5886  elmpocl  6248  relmptopab  6255  funexw  6304  elmpom  6433  mpoxopn0yelv  6469  tfrlem6  6546  funresdfunsndc  6738  pmresg  6909  fundmen  7046  caseinl  7381  caseinr  7382  axaddf  8179  axmulf  8180  hashinfom  11136  4sqlemffi  13087  structcnvcnv  13217  lidlmex  14610  istopon  14865  eltg4i  14907  eltg3  14909  tg1  14911  tg2  14912  tgclb  14917  lmrcl  15044  1vgrex  16002  edg0iedg0g  16048  umgrnloopv  16096  edg0usgr  16229