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

This theorem is referenced by:  f1orel  6777  f1oresrab  7076  fveqf1o  7253  isofrlem  7291  isofr  7293  isose  7294  f1opw  7619  xpcomco  9002  dif1en  9093  f1opwfi  9263  inlresf  9836  inrresf  9838  djuun  9848  isercolllem2  15626  isercoll  15628  unbenlem  16877  gsumpropd2lem  18645  symgfixf1  19410  tgqtop  23702  hmeontr  23759  reghmph  23783  nrmhmph  23784  tgpconncompeqg  24102  cnheiborlem  24946  dfrelog  26554  dvloglem  26637  logf1o2  26639  axcontlem9  29066  axcontlem10  29067  padct  32817  symgcom  33171  cycpmconjvlem  33229  cycpmconjslem2  33243  madjusmdetlem2  34019  tpr2rico  34103  ballotlemrv  34711  reprpmtf1o  34817  hgt750lemg  34845  subfacp1lem2a  35415  subfacp1lem2b  35416  subfacp1lem5  35419  ismtyres  38182  diaclN  41549  dia1elN  41553  diaintclN  41557  docaclN  41623  dibintclN  41666  cantnf2  43777  permaxun  45462  permac8prim  45465  nregmodellem  45467  sge0f1o  46832  f1oresf1o  47760  grimuhgr  48385  uhgrimisgrgric  48429