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

Theorem f1ofun 6280
Description: A one-to-one onto mapping is a function. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1ofun (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)

Proof of Theorem f1ofun
StepHypRef Expression
1 f1ofn 6279 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fnfun 6128 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6025   Fn wfn 6026  1-1-ontowf1o 6030
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 197  df-an 383  df-fn 6034  df-f 6035  df-f1 6036  df-f1o 6038
This theorem is referenced by:  f1orel  6281  f1oresrab  6537  fveqf1o  6700  isofrlem  6733  isofr  6735  isose  6736  f1opw  7036  xpcomco  8206  f1opwfi  8426  inlresf  8940  inrresf  8942  djuun  8952  isercolllem2  14604  isercoll  14606  unbenlem  15819  gsumpropd2lem  17481  symgfixf1  18064  tgqtop  21736  hmeontr  21793  reghmph  21817  nrmhmph  21818  tgpconncompeqg  22135  cnheiborlem  22973  dfrelog  24533  dvloglem  24615  logf1o2  24617  axcontlem9  26073  axcontlem10  26074  padct  29837  madjusmdetlem2  30234  tpr2rico  30298  ballotlemrv  30921  reprpmtf1o  31044  hgt750lemg  31072  subfacp1lem2a  31500  subfacp1lem2b  31501  subfacp1lem5  31504  ismtyres  33939  diaclN  36860  dia1elN  36864  diaintclN  36868  docaclN  36934  dibintclN  36977  sge0f1o  41116  f1oresf1o  41832  f1oresf1o2  41833
  Copyright terms: Public domain W3C validator