Theorem f1ofun 6804

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

Syntax hints:   → wi 4  Fun wfun 6511   Fn wfn 6512  –1-1-onto→wf1o 6516

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 209  df-an 400  df-fn 6520  df-f 6521  df-f1 6522  df-f1o 6524

This theorem is referenced by:  f1orel  6805  f1oresrab  7105  fveqf1o  7282  isofrlem  7320  isofr  7322  isose  7323  f1opw  7648  xpcomco  9035  dif1en  9126  f1opwfi  9296  inlresf  9869  inrresf  9871  djuun  9881  isercolllem2  15676  isercoll  15678  unbenlem  16927  gsumpropd2lem  18696  symgfixf1  19460  tgqtop  23752  hmeontr  23809  reghmph  23833  nrmhmph  23834  tgpconncompeqg  24152  cnheiborlem  24996  dfrelog  26607  dvloglem  26690  logf1o2  26692  axcontlem9  29119  axcontlem10  29120  padct  32870  symgcom  33224  cycpmconjvlem  33282  cycpmconjslem2  33296  madjusmdetlem2  34086  tpr2rico  34170  ballotlemrv  34778  reprpmtf1o  34884  hgt750lemg  34912  subfacp1lem2a  35494  subfacp1lem2b  35495  subfacp1lem5  35498  ismtyres  38271  diaclN  41638  dia1elN  41642  diaintclN  41646  docaclN  41712  dibintclN  41755  cantnf2  43866  permaxun  45551  permac8prim  45554  nregmodellem  45556  sge0f1o  46920  f1oresf1o  47848  grimuhgr  48473  uhgrimisgrgric  48517