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

Theorem f1ofun 6611
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 6610 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fnfun 6447 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6343   Fn wfn 6344  1-1-ontowf1o 6348
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 208  df-an 397  df-fn 6352  df-f 6353  df-f1 6354  df-f1o 6356
This theorem is referenced by:  f1orel  6612  f1oresrab  6882  fveqf1o  7049  isofrlem  7082  isofr  7084  isose  7085  f1opw  7390  xpcomco  8596  f1opwfi  8817  inlresf  9332  inrresf  9334  djuun  9344  isercolllem2  15012  isercoll  15014  unbenlem  16234  gsumpropd2lem  17879  symgfixf1  18496  tgqtop  22250  hmeontr  22307  reghmph  22331  nrmhmph  22332  tgpconncompeqg  22649  cnheiborlem  23487  dfrelog  25076  dvloglem  25158  logf1o2  25160  axcontlem9  26686  axcontlem10  26687  padct  30382  symgcom  30655  cycpmconjvlem  30711  cycpmconjslem2  30725  madjusmdetlem2  30993  tpr2rico  31055  ballotlemrv  31677  reprpmtf1o  31797  hgt750lemg  31825  subfacp1lem2a  32325  subfacp1lem2b  32326  subfacp1lem5  32329  ismtyres  34969  diaclN  38068  dia1elN  38072  diaintclN  38076  docaclN  38142  dibintclN  38185  sge0f1o  42545  f1oresf1o  43370
  Copyright terms: Public domain W3C validator