Theorem f1ofun 6782

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

Syntax hints:   → wi 4  Fun wfun 6492   Fn wfn 6493  –1-1-onto→wf1o 6497

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 6501  df-f 6502  df-f1 6503  df-f1o 6505

This theorem is referenced by:  f1orel  6783  f1oresrab  7080  fveqf1o  7257  isofrlem  7295  isofr  7297  isose  7298  f1opw  7623  xpcomco  9005  dif1en  9096  f1opwfi  9266  inlresf  9838  inrresf  9840  djuun  9850  isercolllem2  15628  isercoll  15630  unbenlem  16879  gsumpropd2lem  18647  symgfixf1  19412  tgqtop  23677  hmeontr  23734  reghmph  23758  nrmhmph  23759  tgpconncompeqg  24077  cnheiborlem  24921  dfrelog  26529  dvloglem  26612  logf1o2  26614  axcontlem9  29041  axcontlem10  29042  padct  32791  symgcom  33144  cycpmconjvlem  33202  cycpmconjslem2  33216  madjusmdetlem2  33972  tpr2rico  34056  ballotlemrv  34664  reprpmtf1o  34770  hgt750lemg  34798  subfacp1lem2a  35362  subfacp1lem2b  35363  subfacp1lem5  35366  ismtyres  38129  diaclN  41496  dia1elN  41500  diaintclN  41504  docaclN  41570  dibintclN  41613  cantnf2  43753  permaxun  45438  permac8prim  45441  nregmodellem  45443  sge0f1o  46810  f1oresf1o  47738  grimuhgr  48363  uhgrimisgrgric  48407