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  7065  fveqf1o  7243  isofrlem  7281  isofr  7283  isose  7284  f1opw  7609  xpcomco  8991  dif1en  9084  dif1enOLD  9086  f1opwfi  9265  inlresf  9829  inrresf  9831  djuun  9841  isercolllem2  15591  isercoll  15593  unbenlem  16838  gsumpropd2lem  18571  symgfixf1  19334  tgqtop  23615  hmeontr  23672  reghmph  23696  nrmhmph  23697  tgpconncompeqg  24015  cnheiborlem  24869  dfrelog  26490  dvloglem  26573  logf1o2  26575  axcontlem9  28935  axcontlem10  28936  padct  32676  symgcom  33038  cycpmconjvlem  33096  cycpmconjslem2  33110  madjusmdetlem2  33794  tpr2rico  33878  ballotlemrv  34487  reprpmtf1o  34593  hgt750lemg  34621  subfacp1lem2a  35152  subfacp1lem2b  35153  subfacp1lem5  35156  ismtyres  37787  diaclN  41029  dia1elN  41033  diaintclN  41037  docaclN  41103  dibintclN  41146  cantnf2  43298  permaxun  44985  permac8prim  44988  nregmodellem  44990  sge0f1o  46364  f1oresf1o  47275  grimuhgr  47872  uhgrimisgrgric  47916