Theorem f1ofun 6850

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

Syntax hints:   → wi 4  Fun wfun 6555   Fn wfn 6556  –1-1-onto→wf1o 6560

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 6564  df-f 6565  df-f1 6566  df-f1o 6568

This theorem is referenced by:  f1orel  6851  f1oresrab  7147  fveqf1o  7322  isofrlem  7360  isofr  7362  isose  7363  f1opw  7689  xpcomco  9102  dif1en  9200  dif1enOLD  9202  f1opwfi  9396  inlresf  9954  inrresf  9956  djuun  9966  isercolllem2  15702  isercoll  15704  unbenlem  16946  gsumpropd2lem  18692  symgfixf1  19455  tgqtop  23720  hmeontr  23777  reghmph  23801  nrmhmph  23802  tgpconncompeqg  24120  cnheiborlem  24986  dfrelog  26607  dvloglem  26690  logf1o2  26692  axcontlem9  28987  axcontlem10  28988  padct  32731  symgcom  33103  cycpmconjvlem  33161  cycpmconjslem2  33175  madjusmdetlem2  33827  tpr2rico  33911  ballotlemrv  34522  reprpmtf1o  34641  hgt750lemg  34669  subfacp1lem2a  35185  subfacp1lem2b  35186  subfacp1lem5  35189  ismtyres  37815  diaclN  41052  dia1elN  41056  diaintclN  41060  docaclN  41126  dibintclN  41169  cantnf2  43338  sge0f1o  46397  f1oresf1o  47302  uspgrimprop  47873  grimuhgr  47878  uhgrimisgrgric  47899