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

Theorem f1ofun 6766
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 6765 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fnfun 6582 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6476   Fn wfn 6477  1-1-ontowf1o 6481
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 6485  df-f 6486  df-f1 6487  df-f1o 6489
This theorem is referenced by:  f1orel  6767  f1oresrab  7061  fveqf1o  7239  isofrlem  7277  isofr  7279  isose  7280  f1opw  7605  xpcomco  8984  dif1en  9075  f1opwfi  9246  inlresf  9810  inrresf  9812  djuun  9822  isercolllem2  15573  isercoll  15575  unbenlem  16820  gsumpropd2lem  18553  symgfixf1  19316  tgqtop  23597  hmeontr  23654  reghmph  23678  nrmhmph  23679  tgpconncompeqg  23997  cnheiborlem  24851  dfrelog  26472  dvloglem  26555  logf1o2  26557  axcontlem9  28917  axcontlem10  28918  padct  32662  symgcom  33025  cycpmconjvlem  33083  cycpmconjslem2  33097  madjusmdetlem2  33795  tpr2rico  33879  ballotlemrv  34488  reprpmtf1o  34594  hgt750lemg  34622  subfacp1lem2a  35153  subfacp1lem2b  35154  subfacp1lem5  35157  ismtyres  37788  diaclN  41029  dia1elN  41033  diaintclN  41037  docaclN  41103  dibintclN  41146  cantnf2  43298  permaxun  44985  permac8prim  44988  nregmodellem  44990  sge0f1o  46363  f1oresf1o  47274  grimuhgr  47871  uhgrimisgrgric  47915
  Copyright terms: Public domain W3C validator