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

Theorem f1orel 6837
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 6836 . 2 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
2 funrel 6566 . 2 (Fun 𝐹 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Rel 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Rel wrel 5682  Fun wfun 6538  1-1-ontowf1o 6543
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 206  df-an 398  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-f1o 6551
This theorem is referenced by:  f1ococnv1  6863  isores1  7331  weisoeq2  7353  f1oexrnex  7918  ssenen  9151  f1oenfirn  9183  cantnffval2  9690  hasheqf1oi  14311  cmphaushmeo  23304  cycpmconjs  32315  poimirlem3  36491  f1ocan2fv  36595  ltrncnvnid  38998  brco2f1o  42783  brco3f1o  42784  ntrclsnvobr  42803  ntrclsiex  42804  ntrneiiex  42827  ntrneinex  42828  neicvgel1  42870
  Copyright terms: Public domain W3C validator