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

Theorem f1orel 6359
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 6358 . 2 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
2 funrel 6118 . 2 (Fun 𝐹 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Rel 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Rel wrel 5317  Fun wfun 6095  1-1-ontowf1o 6100
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 199  df-an 386  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-f1o 6108
This theorem is referenced by:  f1ococnv1  6384  isores1  6812  weisoeq2  6834  f1oexrnex  7350  ssenen  8376  cantnffval2  8842  hasheqf1oi  13392  cmphaushmeo  21932  poimirlem3  33901  f1ocan2fv  34010  ltrncnvnid  36148  brco2f1o  39112  brco3f1o  39113  ntrclsnvobr  39132  ntrclsiex  39133  ntrneiiex  39156  ntrneinex  39157  neicvgel1  39199
  Copyright terms: Public domain W3C validator