Theorem f1ofun 6823

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6531   Fn wfn 6532  –1-1-onto→wf1o 6536

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 6540  df-f 6541  df-f1 6542  df-f1o 6544

This theorem is used by:  f1orel  6824  f1oresrab  7125  fveqf1o  7307  isofrlem  7345  isofr  7347  isose  7348  f1opw  7674  xpcomco  9069  dif1en  9160  f1opwfi  9327  inlresf  9923  inrresf  9925  djuun  9935  isercolllem2  15757  isercoll  15759  unbenlem  17006  gsumpropd2lem  18787  symgfixf1  19570  tgqtop  23944  hmeontr  24001  reghmph  24025  nrmhmph  24026  tgpconncompeqg  24344  cnheiborlem  25188  dfrelog  26810  dvloglem  26893  logf1o2  26895  axcontlem9  29437  axcontlem10  29438  padct  33197  symgcom  33531  cycpmconjvlem  33589  cycpmconjslem2  33603  madjusmdetlem2  34346  tpr2rico  34430  ballotlemrv  35039  reprpmtf1o  35142  hgt750lemg  35170  subfacp1lem2a  35767  subfacp1lem2b  35768  subfacp1lem5  35771  ismtyres  38566  diaclN  41931  dia1elN  41935  diaintclN  41939  docaclN  42005  dibintclN  42048  cantnf2  44174  permaxun  45842  permac8prim  45845  nregmodellem  45847  sge0f1o  47218  f1oresf1o  48186  grimuhgr  48811  uhgrimisgrgric  48855