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

Theorem f1orel 6669
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 6668 . 2 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
2 funrel 6402 . 2 (Fun 𝐹 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Rel 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Rel wrel 5561  Fun wfun 6379  1-1-ontowf1o 6384
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 400  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-f1o 6392
This theorem is referenced by:  f1ococnv1  6694  isores1  7148  weisoeq2  7170  f1oexrnex  7710  ssenen  8825  f1oenfirn  8865  cantnffval2  9315  hasheqf1oi  13923  cmphaushmeo  22702  cycpmconjs  31147  poimirlem3  35522  f1ocan2fv  35627  ltrncnvnid  37883  brco2f1o  41327  brco3f1o  41328  ntrclsnvobr  41347  ntrclsiex  41348  ntrneiiex  41371  ntrneinex  41372  neicvgel1  41414
  Copyright terms: Public domain W3C validator