Theorem f1ofun 6770

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

Syntax hints:   → wi 4  Fun wfun 6480   Fn wfn 6481  –1-1-onto→wf1o 6485

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 207  df-an 396  df-fn 6489  df-f 6490  df-f1 6491  df-f1o 6493

This theorem is referenced by:  f1orel  6771  f1oresrab  7066  fveqf1o  7242  isofrlem  7280  isofr  7282  isose  7283  f1opw  7608  xpcomco  8987  dif1en  9078  f1opwfi  9247  inlresf  9814  inrresf  9816  djuun  9826  isercolllem2  15575  isercoll  15577  unbenlem  16822  gsumpropd2lem  18589  symgfixf1  19351  tgqtop  23628  hmeontr  23685  reghmph  23709  nrmhmph  23710  tgpconncompeqg  24028  cnheiborlem  24881  dfrelog  26502  dvloglem  26585  logf1o2  26587  axcontlem9  28952  axcontlem10  28953  padct  32705  symgcom  33059  cycpmconjvlem  33117  cycpmconjslem2  33131  madjusmdetlem2  33862  tpr2rico  33946  ballotlemrv  34554  reprpmtf1o  34660  hgt750lemg  34688  subfacp1lem2a  35245  subfacp1lem2b  35246  subfacp1lem5  35249  ismtyres  37869  diaclN  41170  dia1elN  41174  diaintclN  41178  docaclN  41244  dibintclN  41287  cantnf2  43443  permaxun  45129  permac8prim  45132  nregmodellem  45134  sge0f1o  46505  f1oresf1o  47415  grimuhgr  48012  uhgrimisgrgric  48056