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

Theorem f1orel 6053
 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 6052 . 2 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
2 funrel 5821 . 2 (Fun 𝐹 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Rel 𝐹)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  Rel wrel 5043  Fun wfun 5798  –1-1-onto→wf1o 5803 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 196  df-an 385  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-f1o 5811 This theorem is referenced by:  f1ococnv1  6078  isores1  6484  weisoeq2  6506  f1oexrnex  7008  ssenen  8019  cantnffval2  8475  hasheqf1oi  13002  hasheqf1oiOLD  13003  cmphaushmeo  21413  poimirlem3  32582  f1ocan2fv  32692  ltrncnvnid  34431  brco2f1o  37350  brco3f1o  37351  ntrclsnvobr  37370  ntrclsiex  37371  ntrneiiex  37394  ntrneinex  37395  neicvgel1  37437
 Copyright terms: Public domain W3C validator