Theorem f1ofun 6619

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

Syntax hints:   → wi 4  Fun wfun 6351   Fn wfn 6352  –1-1-onto→wf1o 6356

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 209  df-an 399  df-fn 6360  df-f 6361  df-f1 6362  df-f1o 6364

This theorem is referenced by:  f1orel  6620  f1oresrab  6891  fveqf1o  7060  isofrlem  7095  isofr  7097  isose  7098  f1opw  7403  xpcomco  8609  f1opwfi  8830  inlresf  9345  inrresf  9347  djuun  9357  isercolllem2  15024  isercoll  15026  unbenlem  16246  gsumpropd2lem  17891  symgfixf1  18567  tgqtop  22322  hmeontr  22379  reghmph  22403  nrmhmph  22404  tgpconncompeqg  22722  cnheiborlem  23560  dfrelog  25151  dvloglem  25233  logf1o2  25235  axcontlem9  26760  axcontlem10  26761  padct  30457  symgcom  30729  cycpmconjvlem  30785  cycpmconjslem2  30799  madjusmdetlem2  31095  tpr2rico  31157  ballotlemrv  31779  reprpmtf1o  31899  hgt750lemg  31927  subfacp1lem2a  32429  subfacp1lem2b  32430  subfacp1lem5  32433  ismtyres  35088  diaclN  38188  dia1elN  38192  diaintclN  38196  docaclN  38262  dibintclN  38305  sge0f1o  42671  f1oresf1o  43496