Theorem f1ofun 6280

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

Syntax hints:   → wi 4  Fun wfun 6025   Fn wfn 6026  –1-1-onto→wf1o 6030

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 197  df-an 383  df-fn 6034  df-f 6035  df-f1 6036  df-f1o 6038

This theorem is referenced by:  f1orel  6281  f1oresrab  6537  fveqf1o  6700  isofrlem  6733  isofr  6735  isose  6736  f1opw  7036  xpcomco  8206  f1opwfi  8426  inlresf  8940  inrresf  8942  djuun  8952  isercolllem2  14604  isercoll  14606  unbenlem  15819  gsumpropd2lem  17481  symgfixf1  18064  tgqtop  21736  hmeontr  21793  reghmph  21817  nrmhmph  21818  tgpconncompeqg  22135  cnheiborlem  22973  dfrelog  24533  dvloglem  24615  logf1o2  24617  axcontlem9  26073  axcontlem10  26074  padct  29837  madjusmdetlem2  30234  tpr2rico  30298  ballotlemrv  30921  reprpmtf1o  31044  hgt750lemg  31072  subfacp1lem2a  31500  subfacp1lem2b  31501  subfacp1lem5  31504  ismtyres  33939  diaclN  36860  dia1elN  36864  diaintclN  36868  docaclN  36934  dibintclN  36977  sge0f1o  41116  f1oresf1o  41832  f1oresf1o2  41833