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

Theorem f1orel 6301
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 6300 . 2 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
2 funrel 6066 . 2 (Fun 𝐹 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Rel 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Rel wrel 5271  Fun wfun 6043  1-1-ontowf1o 6048
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 385  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-f1o 6056
This theorem is referenced by:  f1ococnv1  6326  isores1  6747  weisoeq2  6769  f1oexrnex  7280  ssenen  8299  cantnffval2  8765  hasheqf1oi  13334  cmphaushmeo  21805  poimirlem3  33725  f1ocan2fv  33835  ltrncnvnid  35916  brco2f1o  38832  brco3f1o  38833  ntrclsnvobr  38852  ntrclsiex  38853  ntrneiiex  38876  ntrneinex  38877  neicvgel1  38919
  Copyright terms: Public domain W3C validator