Theorem f1ofun 6766

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

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

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 6485  df-f 6486  df-f1 6487  df-f1o 6489

This theorem is referenced by:  f1orel  6767  f1oresrab  7061  fveqf1o  7239  isofrlem  7277  isofr  7279  isose  7280  f1opw  7605  xpcomco  8984  dif1en  9075  f1opwfi  9246  inlresf  9810  inrresf  9812  djuun  9822  isercolllem2  15573  isercoll  15575  unbenlem  16820  gsumpropd2lem  18553  symgfixf1  19316  tgqtop  23597  hmeontr  23654  reghmph  23678  nrmhmph  23679  tgpconncompeqg  23997  cnheiborlem  24851  dfrelog  26472  dvloglem  26555  logf1o2  26557  axcontlem9  28917  axcontlem10  28918  padct  32662  symgcom  33025  cycpmconjvlem  33083  cycpmconjslem2  33097  madjusmdetlem2  33795  tpr2rico  33879  ballotlemrv  34488  reprpmtf1o  34594  hgt750lemg  34622  subfacp1lem2a  35153  subfacp1lem2b  35154  subfacp1lem5  35157  ismtyres  37788  diaclN  41029  dia1elN  41033  diaintclN  41037  docaclN  41103  dibintclN  41146  cantnf2  43298  permaxun  44985  permac8prim  44988  nregmodellem  44990  sge0f1o  46363  f1oresf1o  47274  grimuhgr  47871  uhgrimisgrgric  47915