Theorem f1ofun 6393

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

Syntax hints:   → wi 4  Fun wfun 6129   Fn wfn 6130  –1-1-onto→wf1o 6134

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 199  df-an 387  df-fn 6138  df-f 6139  df-f1 6140  df-f1o 6142

This theorem is referenced by:  f1orel  6394  f1oresrab  6659  fveqf1o  6829  isofrlem  6862  isofr  6864  isose  6865  f1opw  7166  xpcomco  8338  f1opwfi  8558  inlresf  9073  inrresf  9075  djuun  9085  isercolllem2  14804  isercoll  14806  unbenlem  16016  gsumpropd2lem  17659  symgfixf1  18240  tgqtop  21924  hmeontr  21981  reghmph  22005  nrmhmph  22006  tgpconncompeqg  22323  cnheiborlem  23161  dfrelog  24749  dvloglem  24831  logf1o2  24833  axcontlem9  26321  axcontlem10  26322  padct  30063  madjusmdetlem2  30492  tpr2rico  30556  ballotlemrv  31180  reprpmtf1o  31306  hgt750lemg  31334  subfacp1lem2a  31761  subfacp1lem2b  31762  subfacp1lem5  31765  ismtyres  34231  diaclN  37204  dia1elN  37208  diaintclN  37212  docaclN  37278  dibintclN  37321  sge0f1o  41523  f1oresf1o  42331  f1oresf1o2  42332