Theorem f1ofun 6864

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

Syntax hints:   → wi 4  Fun wfun 6567   Fn wfn 6568  –1-1-onto→wf1o 6572

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 6576  df-f 6577  df-f1 6578  df-f1o 6580

This theorem is referenced by:  f1orel  6865  f1oresrab  7161  fveqf1o  7338  isofrlem  7376  isofr  7378  isose  7379  f1opw  7706  xpcomco  9128  dif1en  9226  dif1enOLD  9228  f1opwfi  9426  inlresf  9983  inrresf  9985  djuun  9995  isercolllem2  15714  isercoll  15716  unbenlem  16955  gsumpropd2lem  18717  symgfixf1  19479  tgqtop  23741  hmeontr  23798  reghmph  23822  nrmhmph  23823  tgpconncompeqg  24141  cnheiborlem  25005  dfrelog  26625  dvloglem  26708  logf1o2  26710  axcontlem9  29005  axcontlem10  29006  padct  32733  symgcom  33076  cycpmconjvlem  33134  cycpmconjslem2  33148  madjusmdetlem2  33774  tpr2rico  33858  ballotlemrv  34484  reprpmtf1o  34603  hgt750lemg  34631  subfacp1lem2a  35148  subfacp1lem2b  35149  subfacp1lem5  35152  ismtyres  37768  diaclN  41007  dia1elN  41011  diaintclN  41015  docaclN  41081  dibintclN  41124  cantnf2  43287  sge0f1o  46303  f1oresf1o  47205  uspgrimprop  47757  grimuhgr  47762  uhgrimisgrgric  47783