Theorem f1ofun 6851

Description: A one-to-one onto mapping is a function. (Contributed by NM, 12-Dec-2003.)

Assertion

Ref	Expression
f1ofun	⊢ (𝐹:𝐴⟶1-1onto𝐵 → Fun 𝐹)

Proof of Theorem f1ofun

Step	Hyp	Ref	Expression
1		f1ofn 6850	. 2 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → 𝐹 Fn 𝐴)
2		fnfun 6664	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
3	1, 2	syl 18	1 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → Fun 𝐹)

This proof depends on syntax axioms:   → wi 4  Fun wfun 6555   Fn wfn 6556  ⟶1-1ontowf1o 6560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6564  df-f 6565  df-f1 6566  df-f1o 6568

This theorem is used by:  f1orel  6852  f1oresrab  7155  fveqf1o  7336  isofrlem  7374  isofr  7376  isose  7377  f1opw  7704  xpcomco  9117  dif1en  9208  f1opwfi  9376  inlresf  10025  inrresf  10027  djuun  10037  isercolllem2  15865  isercoll  15867  unbenlem  17118  gsumpropd2lem  18900  symgfixf1  19684  tgqtop  24064  hmeontr  24121  reghmph  24145  nrmhmph  24146  tgpconncompeqg  24464  cnheiborlem  25308  dfrelog  26926  dvloglem  27009  logf1o2  27011  axcontlem9  29583  axcontlem10  29584  padct  33384  symgcom  33720  cycpmconjvlem  33778  cycpmconjslem2  33792  madjusmdetlem2  34543  tpr2rico  34627  ballotlemrv  35235  reprpmtf1o  35338  hgt750lemg  35366  onprcf1of1orbd  36067  subfacp1lem2a  36125  subfacp1lem2b  36126  subfacp1lem5  36129  ismtyres  38945  diaclN  42310  dia1elN  42314  diaintclN  42318  docaclN  42384  dibintclN  42427  cantnf2  44530  permaxun  46207  permac8prim  46210  nregmodellem  46212  hfstructcan  46240  sge0f1o  47607  f1oresf1o  48575  grimuhgr  49200  uhgrimisgrgric  49244