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

Theorem f1ofun 6850
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 6849 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fnfun 6668 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6555   Fn wfn 6556  1-1-ontowf1o 6560
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 6564  df-f 6565  df-f1 6566  df-f1o 6568
This theorem is referenced by:  f1orel  6851  f1oresrab  7147  fveqf1o  7322  isofrlem  7360  isofr  7362  isose  7363  f1opw  7689  xpcomco  9102  dif1en  9200  dif1enOLD  9202  f1opwfi  9396  inlresf  9954  inrresf  9956  djuun  9966  isercolllem2  15702  isercoll  15704  unbenlem  16946  gsumpropd2lem  18692  symgfixf1  19455  tgqtop  23720  hmeontr  23777  reghmph  23801  nrmhmph  23802  tgpconncompeqg  24120  cnheiborlem  24986  dfrelog  26607  dvloglem  26690  logf1o2  26692  axcontlem9  28987  axcontlem10  28988  padct  32731  symgcom  33103  cycpmconjvlem  33161  cycpmconjslem2  33175  madjusmdetlem2  33827  tpr2rico  33911  ballotlemrv  34522  reprpmtf1o  34641  hgt750lemg  34669  subfacp1lem2a  35185  subfacp1lem2b  35186  subfacp1lem5  35189  ismtyres  37815  diaclN  41052  dia1elN  41056  diaintclN  41060  docaclN  41126  dibintclN  41169  cantnf2  43338  sge0f1o  46397  f1oresf1o  47302  uspgrimprop  47873  grimuhgr  47878  uhgrimisgrgric  47899
  Copyright terms: Public domain W3C validator