Theorem f1ofun 6812

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

Syntax hints:   → wi 4  Fun wfun 6519   Fn wfn 6520  –1-1-onto→wf1o 6524

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 401  df-fn 6528  df-f 6529  df-f1 6530  df-f1o 6532

This theorem is referenced by:  f1orel  6813  f1oresrab  7113  fveqf1o  7290  isofrlem  7328  isofr  7330  isose  7331  f1opw  7656  xpcomco  9043  dif1en  9134  f1opwfi  9301  inlresf  9888  inrresf  9890  djuun  9900  isercolllem2  15707  isercoll  15709  unbenlem  16958  gsumpropd2lem  18727  symgfixf1  19498  tgqtop  23830  hmeontr  23887  reghmph  23911  nrmhmph  23912  tgpconncompeqg  24230  cnheiborlem  25074  dfrelog  26688  dvloglem  26771  logf1o2  26773  axcontlem9  29231  axcontlem10  29232  padct  32975  symgcom  33316  cycpmconjvlem  33374  cycpmconjslem2  33388  madjusmdetlem2  34135  tpr2rico  34219  ballotlemrv  34827  reprpmtf1o  34930  hgt750lemg  34958  subfacp1lem2a  35543  subfacp1lem2b  35544  subfacp1lem5  35547  ismtyres  38319  diaclN  41686  dia1elN  41690  diaintclN  41694  docaclN  41760  dibintclN  41803  cantnf2  43914  permaxun  45585  permac8prim  45588  nregmodellem  45590  sge0f1o  46954  f1oresf1o  47882  grimuhgr  48507  uhgrimisgrgric  48551