Theorem f1ofun 6836

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

Syntax hints:   → wi 4  Fun wfun 6538   Fn wfn 6539  –1-1-onto→wf1o 6543

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 206  df-an 398  df-fn 6547  df-f 6548  df-f1 6549  df-f1o 6551

This theorem is referenced by:  f1orel  6837  f1oresrab  7125  fveqf1o  7301  isofrlem  7337  isofr  7339  isose  7340  f1opw  7662  xpcomco  9062  dif1en  9160  dif1enOLD  9162  f1opwfi  9356  inlresf  9909  inrresf  9911  djuun  9921  isercolllem2  15612  isercoll  15614  unbenlem  16841  gsumpropd2lem  18598  symgfixf1  19305  tgqtop  23216  hmeontr  23273  reghmph  23297  nrmhmph  23298  tgpconncompeqg  23616  cnheiborlem  24470  dfrelog  26074  dvloglem  26156  logf1o2  26158  axcontlem9  28230  axcontlem10  28231  padct  31944  symgcom  32244  cycpmconjvlem  32300  cycpmconjslem2  32314  madjusmdetlem2  32808  tpr2rico  32892  ballotlemrv  33518  reprpmtf1o  33638  hgt750lemg  33666  subfacp1lem2a  34171  subfacp1lem2b  34172  subfacp1lem5  34175  ismtyres  36676  diaclN  39921  dia1elN  39925  diaintclN  39929  docaclN  39995  dibintclN  40038  cantnf2  42075  sge0f1o  45098  f1oresf1o  45998