Theorem f1ofun 6829

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6537   Fn wfn 6538  –1-1-onto→wf1o 6542

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6546  df-f 6547  df-f1 6548  df-f1o 6550

This theorem is used by:  f1orel  6830  f1oresrab  7130  fveqf1o  7311  isofrlem  7349  isofr  7351  isose  7352  f1opw  7679  xpcomco  9065  dif1en  9156  f1opwfi  9323  inlresf  9919  inrresf  9921  djuun  9931  isercolllem2  15743  isercoll  15745  unbenlem  16993  gsumpropd2lem  18766  symgfixf1  19538  tgqtop  23906  hmeontr  23963  reghmph  23987  nrmhmph  23988  tgpconncompeqg  24306  cnheiborlem  25150  dfrelog  26767  dvloglem  26850  logf1o2  26852  axcontlem9  29359  axcontlem10  29360  padct  33100  symgcom  33434  cycpmconjvlem  33492  cycpmconjslem2  33506  madjusmdetlem2  34249  tpr2rico  34333  ballotlemrv  34942  reprpmtf1o  35045  hgt750lemg  35073  subfacp1lem2a  35693  subfacp1lem2b  35694  subfacp1lem5  35697  ismtyres  38500  diaclN  41865  dia1elN  41869  diaintclN  41873  docaclN  41939  dibintclN  41982  cantnf2  44093  permaxun  45761  permac8prim  45764  nregmodellem  45766  sge0f1o  47137  f1oresf1o  48068  grimuhgr  48693  uhgrimisgrgric  48737