Theorem f1ofun 6702

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

Syntax hints:   → wi 4  Fun wfun 6412   Fn wfn 6413  –1-1-onto→wf1o 6417

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 396  df-fn 6421  df-f 6422  df-f1 6423  df-f1o 6425

This theorem is referenced by:  f1orel  6703  f1oresrab  6981  fveqf1o  7155  isofrlem  7191  isofr  7193  isose  7194  f1opw  7503  xpcomco  8802  dif1en  8907  f1opwfi  9053  inlresf  9603  inrresf  9605  djuun  9615  isercolllem2  15305  isercoll  15307  unbenlem  16537  gsumpropd2lem  18278  symgfixf1  18960  tgqtop  22771  hmeontr  22828  reghmph  22852  nrmhmph  22853  tgpconncompeqg  23171  cnheiborlem  24023  dfrelog  25626  dvloglem  25708  logf1o2  25710  axcontlem9  27243  axcontlem10  27244  padct  30956  symgcom  31254  cycpmconjvlem  31310  cycpmconjslem2  31324  madjusmdetlem2  31680  tpr2rico  31764  ballotlemrv  32386  reprpmtf1o  32506  hgt750lemg  32534  subfacp1lem2a  33042  subfacp1lem2b  33043  subfacp1lem5  33046  ismtyres  35893  diaclN  38991  dia1elN  38995  diaintclN  38999  docaclN  39065  dibintclN  39108  sge0f1o  43810  f1oresf1o  44669