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

Theorem funrel 6345
 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 6330 . 2 (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴𝐴) ⊆ I ))
21simplbi 501 1 (Fun 𝐴 → Rel 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ⊆ wss 3884   I cid 5427  ◡ccnv 5522   ∘ ccom 5527  Rel wrel 5528  Fun wfun 6322 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 210  df-an 400  df-fun 6330 This theorem is referenced by:  0nelfun  6346  funeu  6353  nfunv  6361  funopg  6362  funssres  6372  funun  6374  fununfun  6376  fununi  6403  funcnvres2  6408  fnrel  6428  fcoi1  6530  f1orel  6597  funbrfv  6695  funbrfv2b  6702  funfv2  6730  funfvbrb  6802  fimacnvinrn  6821  fvn0ssdmfun  6823  funopsn  6891  funresdfunsn  6932  funexw  7639  funfv1st2nd  7731  funelss  7732  funeldmdif  7733  wfrrel  7947  tfrlem6  8005  tfr2b  8019  pmresg  8421  fundmen  8570  resfifsupp  8849  rankwflemb  9210  gruima  10217  structcnvcnv  16492  inviso1  17031  setciso  17346  edg0iedg0  26851  edg0usgr  27046  usgr1v0edg  27050  fgreu  30438  fressupp  30451  gsumhashmul  30744  cycpmconjvlem  30836  cycpmconjslem2  30850  bnj1379  32210  funen1cnv  32465  fundmpss  33117  funsseq  33119  frrlem6  33236  nolt02o  33307  nosupbnd1  33322  nosupbnd2lem1  33323  nosupbnd2  33324  noetalem2  33326  noetalem3  33327  imageval  33499  imagesset  33522  cocnv  35156  frege124d  40449  frege129d  40451  frege133d  40453  funbrafv  43701  funbrafv2b  43702  funbrafv2  43790  rngciso  44593  rngcisoALTV  44605  ringciso  44644  ringcisoALTV  44668  ackvalsuc0val  45088
 Copyright terms: Public domain W3C validator