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

Theorem f1ofun 6600
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 6599 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fnfun 6436 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6332   Fn wfn 6333  1-1-ontowf1o 6337
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-fn 6341  df-f 6342  df-f1 6343  df-f1o 6345
This theorem is referenced by:  f1orel  6601  f1oresrab  6872  fveqf1o  7042  isofrlem  7077  isofr  7079  isose  7080  f1opw  7386  xpcomco  8592  f1opwfi  8814  inlresf  9329  inrresf  9331  djuun  9341  isercolllem2  15013  isercoll  15015  unbenlem  16233  gsumpropd2lem  17880  symgfixf1  18556  tgqtop  22308  hmeontr  22365  reghmph  22389  nrmhmph  22390  tgpconncompeqg  22708  cnheiborlem  23550  dfrelog  25148  dvloglem  25230  logf1o2  25232  axcontlem9  26757  axcontlem10  26758  padct  30454  symgcom  30747  cycpmconjvlem  30803  cycpmconjslem2  30817  madjusmdetlem2  31116  tpr2rico  31175  ballotlemrv  31797  reprpmtf1o  31917  hgt750lemg  31945  subfacp1lem2a  32447  subfacp1lem2b  32448  subfacp1lem5  32451  ismtyres  35151  diaclN  38251  dia1elN  38255  diaintclN  38259  docaclN  38325  dibintclN  38368  sge0f1o  42878  f1oresf1o  43703
  Copyright terms: Public domain W3C validator