Theorem f1ofun 6824

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

Syntax hints:   → wi 4  Fun wfun 6532   Fn wfn 6533  –1-1-onto→wf1o 6537

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 210  df-an 401  df-fn 6541  df-f 6542  df-f1 6543  df-f1o 6545

This theorem is referenced by:  f1orel  6825  f1oresrab  7125  fveqf1o  7302  isofrlem  7340  isofr  7342  isose  7343  f1opw  7668  xpcomco  9056  dif1en  9147  f1opwfi  9314  inlresf  9901  inrresf  9903  djuun  9913  isercolllem2  15719  isercoll  15721  unbenlem  16969  gsumpropd2lem  18738  symgfixf1  19508  tgqtop  23850  hmeontr  23907  reghmph  23931  nrmhmph  23932  tgpconncompeqg  24250  cnheiborlem  25094  dfrelog  26708  dvloglem  26791  logf1o2  26793  axcontlem9  29300  axcontlem10  29301  padct  33041  symgcom  33381  cycpmconjvlem  33439  cycpmconjslem2  33453  madjusmdetlem2  34196  tpr2rico  34280  ballotlemrv  34888  reprpmtf1o  34991  hgt750lemg  35019  subfacp1lem2a  35650  subfacp1lem2b  35651  subfacp1lem5  35654  ismtyres  38437  diaclN  41802  dia1elN  41806  diaintclN  41810  docaclN  41876  dibintclN  41919  cantnf2  44032  permaxun  45700  permac8prim  45703  nregmodellem  45705  sge0f1o  47076  f1oresf1o  48004  grimuhgr  48629  uhgrimisgrgric  48673