Theorem f1ofun 6776

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

Syntax hints:   → wi 4  Fun wfun 6486   Fn wfn 6487  –1-1-onto→wf1o 6491

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 6495  df-f 6496  df-f1 6497  df-f1o 6499

This theorem is referenced by:  f1orel  6777  f1oresrab  7072  fveqf1o  7248  isofrlem  7286  isofr  7288  isose  7289  f1opw  7614  xpcomco  8995  dif1en  9086  f1opwfi  9256  inlresf  9826  inrresf  9828  djuun  9838  isercolllem2  15589  isercoll  15591  unbenlem  16836  gsumpropd2lem  18604  symgfixf1  19366  tgqtop  23656  hmeontr  23713  reghmph  23737  nrmhmph  23738  tgpconncompeqg  24056  cnheiborlem  24909  dfrelog  26530  dvloglem  26613  logf1o2  26615  axcontlem9  29045  axcontlem10  29046  padct  32797  symgcom  33165  cycpmconjvlem  33223  cycpmconjslem2  33237  madjusmdetlem2  33985  tpr2rico  34069  ballotlemrv  34677  reprpmtf1o  34783  hgt750lemg  34811  subfacp1lem2a  35374  subfacp1lem2b  35375  subfacp1lem5  35378  ismtyres  38005  diaclN  41306  dia1elN  41310  diaintclN  41314  docaclN  41380  dibintclN  41423  cantnf2  43563  permaxun  45248  permac8prim  45251  nregmodellem  45253  sge0f1o  46622  f1oresf1o  47532  grimuhgr  48129  uhgrimisgrgric  48173