Theorem funrel 6372

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

Syntax hints:   → wi 4   ⊆ wss 3936   I cid 5459  ^◡ccnv 5554   ∘ ccom 5559  Rel wrel 5560  Fun wfun 6349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 399  df-fun 6357

This theorem is referenced by:  0nelfun  6373  funeu  6380  nfunv  6388  funopg  6389  funssres  6398  funun  6400  fununfun  6402  fununi  6429  funcnvres2  6434  fnrel  6454  fcoi1  6552  f1orel  6618  funbrfv  6716  funbrfv2b  6723  funfv2  6751  funfvbrb  6821  fimacnvinrn  6840  fvn0ssdmfun  6842  funopsn  6910  funresdfunsn  6951  funexw  7653  funfv1st2nd  7745  funelss  7746  funeldmdif  7747  wfrrel  7960  tfrlem6  8018  tfr2b  8032  pmresg  8434  fundmen  8583  resfifsupp  8861  rankwflemb  9222  gruima  10224  structcnvcnv  16497  inviso1  17036  setciso  17351  edg0iedg0  26840  edg0usgr  27035  usgr1v0edg  27039  fgreu  30417  cycpmconjvlem  30783  cycpmconjslem2  30797  bnj1379  32102  funen1cnv  32357  fundmpss  33009  funsseq  33011  frrlem6  33128  nolt02o  33199  nosupbnd1  33214  nosupbnd2lem1  33215  nosupbnd2  33216  noetalem2  33218  noetalem3  33219  imageval  33391  imagesset  33414  cocnv  35015  frege124d  40155  frege129d  40157  frege133d  40159  funbrafv  43406  funbrafv2b  43407  funbrafv2  43495  rngciso  44302  rngcisoALTV  44314  ringciso  44353  ringcisoALTV  44377