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

Theorem f1orel 6788
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 6787 . 2 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
2 funrel 6519 . 2 (Fun 𝐹 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Rel 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Rel wrel 5639  Fun wfun 6491  1-1-ontowf1o 6496
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 398  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-f1o 6504
This theorem is referenced by:  f1ococnv1  6814  isores1  7280  weisoeq2  7302  f1oexrnex  7865  ssenen  9096  f1oenfirn  9128  cantnffval2  9632  hasheqf1oi  14252  cmphaushmeo  23154  cycpmconjs  32008  poimirlem3  36084  f1ocan2fv  36189  ltrncnvnid  38593  brco2f1o  42311  brco3f1o  42312  ntrclsnvobr  42331  ntrclsiex  42332  ntrneiiex  42355  ntrneinex  42356  neicvgel1  42398
  Copyright terms: Public domain W3C validator