Theorem f1ofun 6139

Description: A one-to-one onto mapping is a function. (Contributed by NM, 12-Dec-2003.)

Assertion

Ref	Expression
f1ofun	|- ( F : A -1-1-onto-> B -> Fun F )

Proof of Theorem f1ofun

Step	Hyp	Ref	Expression
1		f1ofn 6138	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fnfun 5988	. 2 |- ( F Fn A -> Fun F )
3	1, 2	syl 17	1 |- ( F : A -1-1-onto-> B -> Fun F )

Syntax hints:   -> wi 4   Fun wfun 5882   Fn wfn 5883   -1-1-onto->wf1o 5887

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 197  df-an 386  df-fn 5891  df-f 5892  df-f1 5893  df-f1o 5895

This theorem is referenced by:  f1orel  6140  f1oresrab  6395  fveqf1o  6557  isofrlem  6590  isofr  6592  isose  6593  f1opw  6889  xpcomco  8050  f1opwfi  8270  isercolllem2  14396  isercoll  14398  unbenlem  15612  gsumpropd2lem  17273  symgfixf1  17857  tgqtop  21515  hmeontr  21572  reghmph  21596  nrmhmph  21597  tgpconncompeqg  21915  cnheiborlem  22753  dfrelog  24312  dvloglem  24394  logf1o2  24396  axcontlem9  25852  axcontlem10  25853  padct  29497  madjusmdetlem2  29894  tpr2rico  29958  ballotlemrv  30581  reprpmtf1o  30704  hgt750lemg  30732  subfacp1lem2a  31162  subfacp1lem2b  31163  subfacp1lem5  31166  ismtyres  33607  diaclN  36339  dia1elN  36343  diaintclN  36347  docaclN  36413  dibintclN  36456  sge0f1o  40599