Theorem f1ofun 6834

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

Syntax hints:   → wi 4  Fun wfun 6536   Fn wfn 6537  –1-1-onto→wf1o 6541

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 395  df-fn 6545  df-f 6546  df-f1 6547  df-f1o 6549

This theorem is referenced by:  f1orel  6835  f1oresrab  7126  fveqf1o  7303  isofrlem  7339  isofr  7341  isose  7342  f1opw  7664  xpcomco  9064  dif1en  9162  dif1enOLD  9164  f1opwfi  9358  inlresf  9911  inrresf  9913  djuun  9923  isercolllem2  15616  isercoll  15618  unbenlem  16845  gsumpropd2lem  18604  symgfixf1  19346  tgqtop  23436  hmeontr  23493  reghmph  23517  nrmhmph  23518  tgpconncompeqg  23836  cnheiborlem  24700  dfrelog  26310  dvloglem  26392  logf1o2  26394  axcontlem9  28497  axcontlem10  28498  padct  32211  symgcom  32514  cycpmconjvlem  32570  cycpmconjslem2  32584  madjusmdetlem2  33106  tpr2rico  33190  ballotlemrv  33816  reprpmtf1o  33936  hgt750lemg  33964  subfacp1lem2a  34469  subfacp1lem2b  34470  subfacp1lem5  34473  ismtyres  36979  diaclN  40224  dia1elN  40228  diaintclN  40232  docaclN  40298  dibintclN  40341  cantnf2  42377  sge0f1o  45396  f1oresf1o  46296