Theorem f1ofun 6820

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

Syntax hints:   → wi 4  Fun wfun 6525   Fn wfn 6526  –1-1-onto→wf1o 6530

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 6534  df-f 6535  df-f1 6536  df-f1o 6538

This theorem is referenced by:  f1orel  6821  f1oresrab  7117  fveqf1o  7295  isofrlem  7333  isofr  7335  isose  7336  f1opw  7663  xpcomco  9076  dif1en  9174  dif1enOLD  9176  f1opwfi  9368  inlresf  9928  inrresf  9930  djuun  9940  isercolllem2  15682  isercoll  15684  unbenlem  16928  gsumpropd2lem  18657  symgfixf1  19418  tgqtop  23650  hmeontr  23707  reghmph  23731  nrmhmph  23732  tgpconncompeqg  24050  cnheiborlem  24904  dfrelog  26526  dvloglem  26609  logf1o2  26611  axcontlem9  28951  axcontlem10  28952  padct  32697  symgcom  33094  cycpmconjvlem  33152  cycpmconjslem2  33166  madjusmdetlem2  33859  tpr2rico  33943  ballotlemrv  34552  reprpmtf1o  34658  hgt750lemg  34686  subfacp1lem2a  35202  subfacp1lem2b  35203  subfacp1lem5  35206  ismtyres  37832  diaclN  41069  dia1elN  41073  diaintclN  41077  docaclN  41143  dibintclN  41186  cantnf2  43349  permaxun  45036  sge0f1o  46411  f1oresf1o  47319  grimuhgr  47900  uhgrimisgrgric  47944