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

Theorem f1orel 6097
Description: A one-to-one onto mapping is a relation. (Contributed by NM, 13-Dec-2003.)
Assertion
Ref Expression
f1orel (𝐹:𝐴1-1-onto𝐵 → Rel 𝐹)

Proof of Theorem f1orel
StepHypRef Expression
1 f1ofun 6096 . 2 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
2 funrel 5864 . 2 (Fun 𝐹 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Rel 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Rel wrel 5079  Fun wfun 5841  1-1-ontowf1o 5846
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 5849  df-fn 5850  df-f 5851  df-f1 5852  df-f1o 5854
This theorem is referenced by:  f1ococnv1  6122  isores1  6538  weisoeq2  6560  f1oexrnex  7062  ssenen  8078  cantnffval2  8536  hasheqf1oi  13080  hasheqf1oiOLD  13081  cmphaushmeo  21513  poimirlem3  33041  f1ocan2fv  33151  ltrncnvnid  34890  brco2f1o  37809  brco3f1o  37810  ntrclsnvobr  37829  ntrclsiex  37830  ntrneiiex  37853  ntrneinex  37854  neicvgel1  37896
  Copyright terms: Public domain W3C validator