Theorem f1ofun 5823

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

Assertion

Ref	Expression
f1ofun

Proof of Theorem f1ofun

Step	Hyp	Ref	Expression
1		f1ofn 5822	. 2
2		fnfun 5683	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  Funwfun 5587  Fnwfn 5588  -1-1-onto->wf1o 5592

This theorem is referenced by:  f1orel  5824  f1oresrab  6063  fveqf1o  6205  isofrlem  6236  isofr  6238  isose  6239  f1opw  6529  xpcomco  7627  f1opwfi  7844  mapfienOLD  8159  isercolllem2  13488  isercoll  13490  unbenlem  14426  gsumpropd2lem  15900  symgfixf1  16462  tgqtop  20213  hmeontr  20270  reghmph  20294  nrmhmph  20295  tgpconcompeqg  20610  cnheiborlem  21454  dfrelog  22953  dvloglem  23029  logf1o2  23031  axcontlem9  24275  axcontlem10  24276  eupares  24975  eupap1  24976  tpr2rico  27894  ballotlemrv  28458  subfacp1lem2a  28624  subfacp1lem2b  28625  subfacp1lem5  28628  ismtyres  30304  diaclN  36777  dia1elN  36781  diaintclN  36785  docaclN  36851  dibintclN  36894

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 185  df-an 371  df-fn 5596  df-f 5597  df-f1 5598  df-f1o 5600