Theorem f1ofun 6802

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

Syntax hints:   → wi 4  Fun wfun 6505   Fn wfn 6506  –1-1-onto→wf1o 6510

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 6514  df-f 6515  df-f1 6516  df-f1o 6518

This theorem is referenced by:  f1orel  6803  f1oresrab  7099  fveqf1o  7277  isofrlem  7315  isofr  7317  isose  7318  f1opw  7645  xpcomco  9031  dif1en  9124  dif1enOLD  9126  f1opwfi  9307  inlresf  9867  inrresf  9869  djuun  9879  isercolllem2  15632  isercoll  15634  unbenlem  16879  gsumpropd2lem  18606  symgfixf1  19367  tgqtop  23599  hmeontr  23656  reghmph  23680  nrmhmph  23681  tgpconncompeqg  23999  cnheiborlem  24853  dfrelog  26474  dvloglem  26557  logf1o2  26559  axcontlem9  28899  axcontlem10  28900  padct  32643  symgcom  33040  cycpmconjvlem  33098  cycpmconjslem2  33112  madjusmdetlem2  33818  tpr2rico  33902  ballotlemrv  34511  reprpmtf1o  34617  hgt750lemg  34645  subfacp1lem2a  35167  subfacp1lem2b  35168  subfacp1lem5  35171  ismtyres  37802  diaclN  41044  dia1elN  41048  diaintclN  41052  docaclN  41118  dibintclN  41161  cantnf2  43314  permaxun  45001  permac8prim  45004  nregmodellem  45006  sge0f1o  46380  f1oresf1o  47291  grimuhgr  47887  uhgrimisgrgric  47931