Theorem f1ofun 6727

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 6726	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
2		fnfun 6542	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 6431   Fn wfn 6432  –1-1-onto→wf1o 6436

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 6440  df-f 6441  df-f1 6442  df-f1o 6444

This theorem is referenced by:  f1orel  6728  f1oresrab  7008  fveqf1o  7184  isofrlem  7220  isofr  7222  isose  7223  f1opw  7534  xpcomco  8858  dif1en  8954  f1opwfi  9132  inlresf  9681  inrresf  9683  djuun  9693  isercolllem2  15386  isercoll  15388  unbenlem  16618  gsumpropd2lem  18372  symgfixf1  19054  tgqtop  22872  hmeontr  22929  reghmph  22953  nrmhmph  22954  tgpconncompeqg  23272  cnheiborlem  24126  dfrelog  25730  dvloglem  25812  logf1o2  25814  axcontlem9  27349  axcontlem10  27350  padct  31063  symgcom  31361  cycpmconjvlem  31417  cycpmconjslem2  31431  madjusmdetlem2  31787  tpr2rico  31871  ballotlemrv  32495  reprpmtf1o  32615  hgt750lemg  32643  subfacp1lem2a  33151  subfacp1lem2b  33152  subfacp1lem5  33155  ismtyres  35975  diaclN  39071  dia1elN  39075  diaintclN  39079  docaclN  39145  dibintclN  39188  sge0f1o  43927  f1oresf1o  44793