Theorem f1ofun 6765

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

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

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 6484  df-f 6485  df-f1 6486  df-f1o 6488

This theorem is referenced by:  f1orel  6766  f1oresrab  7060  fveqf1o  7236  isofrlem  7274  isofr  7276  isose  7277  f1opw  7602  xpcomco  8980  dif1en  9071  f1opwfi  9240  inlresf  9807  inrresf  9809  djuun  9819  isercolllem2  15573  isercoll  15575  unbenlem  16820  gsumpropd2lem  18587  symgfixf1  19350  tgqtop  23628  hmeontr  23685  reghmph  23709  nrmhmph  23710  tgpconncompeqg  24028  cnheiborlem  24881  dfrelog  26502  dvloglem  26585  logf1o2  26587  axcontlem9  28951  axcontlem10  28952  padct  32699  symgcom  33050  cycpmconjvlem  33108  cycpmconjslem2  33122  madjusmdetlem2  33839  tpr2rico  33923  ballotlemrv  34531  reprpmtf1o  34637  hgt750lemg  34665  subfacp1lem2a  35222  subfacp1lem2b  35223  subfacp1lem5  35226  ismtyres  37854  diaclN  41095  dia1elN  41099  diaintclN  41103  docaclN  41169  dibintclN  41212  cantnf2  43364  permaxun  45050  permac8prim  45053  nregmodellem  45055  sge0f1o  46426  f1oresf1o  47327  grimuhgr  47924  uhgrimisgrgric  47968