Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  funrel Structured version   Visualization version   GIF version

Theorem funrel 5874
 Description: A function is a relation. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
funrel (Fun 𝐴 → Rel 𝐴)

Proof of Theorem funrel
StepHypRef Expression
1 df-fun 5859 . 2 (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴𝐴) ⊆ I ))
21simplbi 476 1 (Fun 𝐴 → Rel 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ⊆ wss 3560   I cid 4994  ◡ccnv 5083   ∘ ccom 5088  Rel wrel 5089  Fun wfun 5851 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 197  df-an 386  df-fun 5859 This theorem is referenced by:  0nelfun  5875  funeu  5882  nfunv  5889  funopg  5890  funssres  5898  funun  5900  fununfun  5902  fununi  5932  funcnvres2  5937  fnrel  5957  fcoi1  6045  f1orel  6107  funbrfv  6201  funbrfv2b  6207  funfv2  6233  funfvbrb  6296  fimacnvinrn  6314  fvn0ssdmfun  6316  funopsn  6378  funresdfunsn  6420  wfrrel  7380  tfrlem6  7438  tfr2b  7452  pmresg  7845  fundmen  7990  resfifsupp  8263  rankwflemb  8616  gruima  9584  structcnvcnv  15813  inviso1  16366  setciso  16681  pmtrsn  17879  00lsp  18921  edg0iedg0  25880  edg0usgr  26072  usgr1v0edg  26076  fmptcof2  29340  fgreu  29355  bnj1379  30662  fundmpss  31421  funsseq  31423  frrlem5b  31539  frrlem6  31543  imageval  31732  imagesset  31755  cocnv  33191  frege124d  37573  frege129d  37575  frege133d  37577  funbrafv  40572  funbrafv2b  40573  rngciso  41300  rngcisoALTV  41312  ringciso  41351  ringcisoALTV  41375
 Copyright terms: Public domain W3C validator