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

Theorem f1ofun 6776
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 6775 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fnfun 6592 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6486   Fn wfn 6487  1-1-ontowf1o 6491
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 207  df-an 396  df-fn 6495  df-f 6496  df-f1 6497  df-f1o 6499
This theorem is referenced by:  f1orel  6777  f1oresrab  7072  fveqf1o  7248  isofrlem  7286  isofr  7288  isose  7289  f1opw  7614  xpcomco  8995  dif1en  9086  f1opwfi  9256  inlresf  9826  inrresf  9828  djuun  9838  isercolllem2  15589  isercoll  15591  unbenlem  16836  gsumpropd2lem  18604  symgfixf1  19366  tgqtop  23656  hmeontr  23713  reghmph  23737  nrmhmph  23738  tgpconncompeqg  24056  cnheiborlem  24909  dfrelog  26530  dvloglem  26613  logf1o2  26615  axcontlem9  29045  axcontlem10  29046  padct  32797  symgcom  33165  cycpmconjvlem  33223  cycpmconjslem2  33237  madjusmdetlem2  33985  tpr2rico  34069  ballotlemrv  34677  reprpmtf1o  34783  hgt750lemg  34811  subfacp1lem2a  35374  subfacp1lem2b  35375  subfacp1lem5  35378  ismtyres  38005  diaclN  41306  dia1elN  41310  diaintclN  41314  docaclN  41380  dibintclN  41423  cantnf2  43563  permaxun  45248  permac8prim  45251  nregmodellem  45253  sge0f1o  46622  f1oresf1o  47532  grimuhgr  48129  uhgrimisgrgric  48173
  Copyright terms: Public domain W3C validator