Theorem f1ofun 6805

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

Syntax hints:   → wi 4  Fun wfun 6508   Fn wfn 6509  –1-1-onto→wf1o 6513

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 6517  df-f 6518  df-f1 6519  df-f1o 6521

This theorem is referenced by:  f1orel  6806  f1oresrab  7102  fveqf1o  7280  isofrlem  7318  isofr  7320  isose  7321  f1opw  7648  xpcomco  9036  dif1en  9130  dif1enOLD  9132  f1opwfi  9314  inlresf  9874  inrresf  9876  djuun  9886  isercolllem2  15639  isercoll  15641  unbenlem  16886  gsumpropd2lem  18613  symgfixf1  19374  tgqtop  23606  hmeontr  23663  reghmph  23687  nrmhmph  23688  tgpconncompeqg  24006  cnheiborlem  24860  dfrelog  26481  dvloglem  26564  logf1o2  26566  axcontlem9  28906  axcontlem10  28907  padct  32650  symgcom  33047  cycpmconjvlem  33105  cycpmconjslem2  33119  madjusmdetlem2  33825  tpr2rico  33909  ballotlemrv  34518  reprpmtf1o  34624  hgt750lemg  34652  subfacp1lem2a  35174  subfacp1lem2b  35175  subfacp1lem5  35178  ismtyres  37809  diaclN  41051  dia1elN  41055  diaintclN  41059  docaclN  41125  dibintclN  41168  cantnf2  43321  permaxun  45008  permac8prim  45011  nregmodellem  45013  sge0f1o  46387  f1oresf1o  47295  grimuhgr  47891  uhgrimisgrgric  47935