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

Theorem f1orel 6611
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 6610 . 2 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
2 funrel 6365 . 2 (Fun 𝐹 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Rel 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Rel wrel 5553  Fun wfun 6342  1-1-ontowf1o 6347
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 6350  df-fn 6351  df-f 6352  df-f1 6353  df-f1o 6355
This theorem is referenced by:  f1ococnv1  6636  isores1  7079  weisoeq2  7101  f1oexrnex  7624  ssenen  8683  cantnffval2  9150  hasheqf1oi  13704  cmphaushmeo  22400  cycpmconjs  30791  poimirlem3  34882  f1ocan2fv  34989  ltrncnvnid  37250  brco2f1o  40367  brco3f1o  40368  ntrclsnvobr  40387  ntrclsiex  40388  ntrneiiex  40411  ntrneinex  40412  neicvgel1  40454
  Copyright terms: Public domain W3C validator