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

Theorem f1orel 6813
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 6812 . 2 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
2 funrel 6542 . 2 (Fun 𝐹 → Rel 𝐹)
31, 2syl 18 1 (𝐹:𝐴1-1-onto𝐵 → Rel 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Rel wrel 5656  Fun wfun 6519  1-1-ontowf1o 6524
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 210  df-an 401  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-f1o 6532
This theorem is referenced by:  f1ococnv1  6840  isores1  7322  weisoeq2  7344  f1oexrnex  7912  ssenen  9127  f1oenfirn  9152  cantnffval2  9652  hasheqf1oi  14375  cmphaushmeo  23914  cycpmconjs  33384  f1ocan2fv  38233  ltrncnvnid  40758  brco2f1o  44615  brco3f1o  44616  ntrclsnvobr  44635  ntrclsiex  44636  ntrneiiex  44659  ntrneinex  44660  neicvgel1  44702  3f1oss1  47668  3f1oss2  47669
  Copyright terms: Public domain W3C validator