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

Theorem f1ofun 6787
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 6786 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fnfun 6603 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6491   Fn wfn 6492  1-1-ontowf1o 6496
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-fn 6500  df-f 6501  df-f1 6502  df-f1o 6504
This theorem is referenced by:  f1orel  6788  f1oresrab  7074  fveqf1o  7250  isofrlem  7286  isofr  7288  isose  7289  f1opw  7610  xpcomco  9007  dif1en  9105  dif1enOLD  9107  f1opwfi  9301  inlresf  9851  inrresf  9853  djuun  9863  isercolllem2  15551  isercoll  15553  unbenlem  16781  gsumpropd2lem  18535  symgfixf1  19220  tgqtop  23066  hmeontr  23123  reghmph  23147  nrmhmph  23148  tgpconncompeqg  23466  cnheiborlem  24320  dfrelog  25924  dvloglem  26006  logf1o2  26008  axcontlem9  27924  axcontlem10  27925  padct  31639  symgcom  31937  cycpmconjvlem  31993  cycpmconjslem2  32007  madjusmdetlem2  32412  tpr2rico  32496  ballotlemrv  33122  reprpmtf1o  33242  hgt750lemg  33270  subfacp1lem2a  33777  subfacp1lem2b  33778  subfacp1lem5  33781  ismtyres  36270  diaclN  39516  dia1elN  39520  diaintclN  39524  docaclN  39590  dibintclN  39633  cantnf2  41662  sge0f1o  44630  f1oresf1o  45529
  Copyright terms: Public domain W3C validator