Theorem f1ofun 6753

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

Step	Hyp	Ref	Expression
1		f1ofn 6752	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
2		fnfun 6569	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 6457   Fn wfn 6458  –1-1-onto→wf1o 6462

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 206  df-an 397  df-fn 6466  df-f 6467  df-f1 6468  df-f1o 6470

This theorem is referenced by:  f1orel  6754  f1oresrab  7036  fveqf1o  7212  isofrlem  7248  isofr  7250  isose  7251  f1opw  7563  xpcomco  8902  dif1en  9000  dif1enOLD  9002  f1opwfi  9191  inlresf  9740  inrresf  9742  djuun  9752  isercolllem2  15446  isercoll  15448  unbenlem  16676  gsumpropd2lem  18430  symgfixf1  19112  tgqtop  22934  hmeontr  22991  reghmph  23015  nrmhmph  23016  tgpconncompeqg  23334  cnheiborlem  24188  dfrelog  25792  dvloglem  25874  logf1o2  25876  axcontlem9  27448  axcontlem10  27449  padct  31162  symgcom  31460  cycpmconjvlem  31516  cycpmconjslem2  31530  madjusmdetlem2  31884  tpr2rico  31968  ballotlemrv  32592  reprpmtf1o  32712  hgt750lemg  32740  subfacp1lem2a  33248  subfacp1lem2b  33249  subfacp1lem5  33252  ismtyres  36026  diaclN  39276  dia1elN  39280  diaintclN  39284  docaclN  39350  dibintclN  39393  sge0f1o  44165  f1oresf1o  45041