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

Theorem f1orel 6841
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 6840 . 2 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
2 funrel 6571 . 2 (Fun 𝐹 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Rel 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Rel wrel 5683  Fun wfun 6543  1-1-ontowf1o 6548
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 206  df-an 395  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-f1o 6556
This theorem is referenced by:  f1ococnv1  6867  isores1  7341  weisoeq2  7363  f1oexrnex  7935  ssenen  9176  f1oenfirn  9208  cantnffval2  9720  hasheqf1oi  14346  cmphaushmeo  23748  cycpmconjs  32969  poimirlem3  37227  f1ocan2fv  37331  ltrncnvnid  39730  brco2f1o  43604  brco3f1o  43605  ntrclsnvobr  43624  ntrclsiex  43625  ntrneiiex  43648  ntrneinex  43649  neicvgel1  43691
  Copyright terms: Public domain W3C validator