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

Theorem f1ofun 6037
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 6036 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fnfun 5888 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 5784   Fn wfn 5785  1-1-ontowf1o 5789
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 195  df-an 384  df-fn 5793  df-f 5794  df-f1 5795  df-f1o 5797
This theorem is referenced by:  f1orel  6038  f1oresrab  6287  fveqf1o  6435  isofrlem  6468  isofr  6470  isose  6471  f1opw  6764  xpcomco  7912  f1opwfi  8130  isercolllem2  14190  isercoll  14192  unbenlem  15396  gsumpropd2lem  17042  symgfixf1  17626  tgqtop  21267  hmeontr  21324  reghmph  21348  nrmhmph  21349  tgpconcompeqg  21667  cnheiborlem  22492  dfrelog  24033  dvloglem  24111  logf1o2  24113  axcontlem9  25570  axcontlem10  25571  eupares  26268  eupap1  26269  padct  28691  madjusmdetlem2  29028  tpr2rico  29092  ballotlemrv  29714  subfacp1lem2a  30222  subfacp1lem2b  30223  subfacp1lem5  30226  ismtyres  32573  diaclN  35153  dia1elN  35157  diaintclN  35161  docaclN  35227  dibintclN  35270  sge0f1o  39072
  Copyright terms: Public domain W3C validator