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

Theorem f1orel 6805
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 6804 . 2 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
2 funrel 6535 . 2 (Fun 𝐹 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Rel 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Rel wrel 5645  Fun wfun 6507  1-1-ontowf1o 6512
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 207  df-an 396  df-fun 6515  df-fn 6516  df-f 6517  df-f1 6518  df-f1o 6520
This theorem is referenced by:  f1ococnv1  6831  isores1  7311  weisoeq2  7333  f1oexrnex  7905  ssenen  9120  f1oenfirn  9149  cantnffval2  9654  hasheqf1oi  14322  cmphaushmeo  23693  cycpmconjs  33119  poimirlem3  37612  f1ocan2fv  37716  ltrncnvnid  40116  brco2f1o  44014  brco3f1o  44015  ntrclsnvobr  44034  ntrclsiex  44035  ntrneiiex  44058  ntrneinex  44059  neicvgel1  44101  3f1oss1  47066  3f1oss2  47067
  Copyright terms: Public domain W3C validator