Theorem f1ofun 6784

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

Syntax hints:   → wi 4  Fun wfun 6494   Fn wfn 6495  –1-1-onto→wf1o 6499

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 6503  df-f 6504  df-f1 6505  df-f1o 6507

This theorem is referenced by:  f1orel  6785  f1oresrab  7082  fveqf1o  7258  isofrlem  7296  isofr  7298  isose  7299  f1opw  7624  xpcomco  9007  dif1en  9098  f1opwfi  9268  inlresf  9838  inrresf  9840  djuun  9850  isercolllem2  15601  isercoll  15603  unbenlem  16848  gsumpropd2lem  18616  symgfixf1  19378  tgqtop  23668  hmeontr  23725  reghmph  23749  nrmhmph  23750  tgpconncompeqg  24068  cnheiborlem  24921  dfrelog  26542  dvloglem  26625  logf1o2  26627  axcontlem9  29057  axcontlem10  29058  padct  32807  symgcom  33176  cycpmconjvlem  33234  cycpmconjslem2  33248  madjusmdetlem2  34005  tpr2rico  34089  ballotlemrv  34697  reprpmtf1o  34803  hgt750lemg  34831  subfacp1lem2a  35393  subfacp1lem2b  35394  subfacp1lem5  35397  ismtyres  38053  diaclN  41420  dia1elN  41424  diaintclN  41428  docaclN  41494  dibintclN  41537  cantnf2  43676  permaxun  45361  permac8prim  45364  nregmodellem  45366  sge0f1o  46734  f1oresf1o  47644  grimuhgr  48241  uhgrimisgrgric  48285