Theorem f1ofun 6851

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

Syntax hints:   → wi 4  Fun wfun 6557   Fn wfn 6558  –1-1-onto→wf1o 6562

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 6566  df-f 6567  df-f1 6568  df-f1o 6570

This theorem is referenced by:  f1orel  6852  f1oresrab  7147  fveqf1o  7322  isofrlem  7360  isofr  7362  isose  7363  f1opw  7689  xpcomco  9101  dif1en  9199  dif1enOLD  9201  f1opwfi  9394  inlresf  9952  inrresf  9954  djuun  9964  isercolllem2  15699  isercoll  15701  unbenlem  16942  gsumpropd2lem  18705  symgfixf1  19470  tgqtop  23736  hmeontr  23793  reghmph  23817  nrmhmph  23818  tgpconncompeqg  24136  cnheiborlem  25000  dfrelog  26622  dvloglem  26705  logf1o2  26707  axcontlem9  29002  axcontlem10  29003  padct  32737  symgcom  33086  cycpmconjvlem  33144  cycpmconjslem2  33158  madjusmdetlem2  33789  tpr2rico  33873  ballotlemrv  34501  reprpmtf1o  34620  hgt750lemg  34648  subfacp1lem2a  35165  subfacp1lem2b  35166  subfacp1lem5  35169  ismtyres  37795  diaclN  41033  dia1elN  41037  diaintclN  41041  docaclN  41107  dibintclN  41150  cantnf2  43315  sge0f1o  46338  f1oresf1o  47240  uspgrimprop  47811  grimuhgr  47816  uhgrimisgrgric  47837