Theorem f1ofun 6052

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

Syntax hints:   → wi 4  Fun wfun 5798   Fn wfn 5799  –1-1-onto→wf1o 5803

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 196  df-an 385  df-fn 5807  df-f 5808  df-f1 5809  df-f1o 5811

This theorem is referenced by:  f1orel  6053  f1oresrab  6302  fveqf1o  6457  isofrlem  6490  isofr  6492  isose  6493  f1opw  6787  xpcomco  7935  f1opwfi  8153  isercolllem2  14244  isercoll  14246  unbenlem  15450  gsumpropd2lem  17096  symgfixf1  17680  tgqtop  21325  hmeontr  21382  reghmph  21406  nrmhmph  21407  tgpconcompeqg  21725  cnheiborlem  22561  dfrelog  24116  dvloglem  24194  logf1o2  24196  axcontlem9  25652  axcontlem10  25653  eupares  26502  eupap1  26503  padct  28885  madjusmdetlem2  29222  tpr2rico  29286  ballotlemrv  29908  subfacp1lem2a  30416  subfacp1lem2b  30417  subfacp1lem5  30420  ismtyres  32777  diaclN  35357  dia1elN  35361  diaintclN  35365  docaclN  35431  dibintclN  35474  sge0f1o  39275