Theorem f1ofun 6776

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

Syntax hints:   → wi 4  Fun wfun 6486   Fn wfn 6487  –1-1-onto→wf1o 6491

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 6495  df-f 6496  df-f1 6497  df-f1o 6499

This theorem is referenced by:  f1orel  6777  f1oresrab  7074  fveqf1o  7250  isofrlem  7288  isofr  7290  isose  7291  f1opw  7616  xpcomco  8998  dif1en  9089  f1opwfi  9259  inlresf  9829  inrresf  9831  djuun  9841  isercolllem2  15619  isercoll  15621  unbenlem  16870  gsumpropd2lem  18638  symgfixf1  19403  tgqtop  23687  hmeontr  23744  reghmph  23768  nrmhmph  23769  tgpconncompeqg  24087  cnheiborlem  24931  dfrelog  26542  dvloglem  26625  logf1o2  26627  axcontlem9  29055  axcontlem10  29056  padct  32806  symgcom  33159  cycpmconjvlem  33217  cycpmconjslem2  33231  madjusmdetlem2  33988  tpr2rico  34072  ballotlemrv  34680  reprpmtf1o  34786  hgt750lemg  34814  subfacp1lem2a  35378  subfacp1lem2b  35379  subfacp1lem5  35382  ismtyres  38143  diaclN  41510  dia1elN  41514  diaintclN  41518  docaclN  41584  dibintclN  41627  cantnf2  43771  permaxun  45456  permac8prim  45459  nregmodellem  45461  sge0f1o  46828  f1oresf1o  47750  grimuhgr  48375  uhgrimisgrgric  48419