Theorem f1ofun 6592

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

Syntax hints:   → wi 4  Fun wfun 6318   Fn wfn 6319  –1-1-onto→wf1o 6323

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 210  df-an 400  df-fn 6327  df-f 6328  df-f1 6329  df-f1o 6331

This theorem is referenced by:  f1orel  6593  f1oresrab  6866  fveqf1o  7037  isofrlem  7072  isofr  7074  isose  7075  f1opw  7381  xpcomco  8590  f1opwfi  8812  inlresf  9327  inrresf  9329  djuun  9339  isercolllem2  15014  isercoll  15016  unbenlem  16234  gsumpropd2lem  17881  symgfixf1  18557  tgqtop  22317  hmeontr  22374  reghmph  22398  nrmhmph  22399  tgpconncompeqg  22717  cnheiborlem  23559  dfrelog  25157  dvloglem  25239  logf1o2  25241  axcontlem9  26766  axcontlem10  26767  padct  30481  symgcom  30777  cycpmconjvlem  30833  cycpmconjslem2  30847  madjusmdetlem2  31181  tpr2rico  31265  ballotlemrv  31887  reprpmtf1o  32007  hgt750lemg  32035  subfacp1lem2a  32540  subfacp1lem2b  32541  subfacp1lem5  32544  ismtyres  35246  diaclN  38346  dia1elN  38350  diaintclN  38354  docaclN  38420  dibintclN  38463  sge0f1o  43021  f1oresf1o  43846