Theorem f1ofun 6818

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 6525   Fn wfn 6526  –1-1-onto→wf1o 6530

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 6534  df-f 6535  df-f1 6536  df-f1o 6538

This theorem is used by:  f1orel  6819  f1oresrab  7120  fveqf1o  7302  isofrlem  7340  isofr  7342  isose  7343  f1opw  7669  xpcomco  9070  dif1en  9161  f1opwfi  9329  inlresf  9976  inrresf  9978  djuun  9988  isercolllem2  15813  isercoll  15815  unbenlem  17066  gsumpropd2lem  18848  symgfixf1  19631  tgqtop  24011  hmeontr  24068  reghmph  24092  nrmhmph  24093  tgpconncompeqg  24411  cnheiborlem  25255  dfrelog  26875  dvloglem  26958  logf1o2  26960  axcontlem9  29532  axcontlem10  29533  padct  33292  symgcom  33626  cycpmconjvlem  33684  cycpmconjslem2  33698  madjusmdetlem2  34442  tpr2rico  34526  ballotlemrv  35135  reprpmtf1o  35238  hgt750lemg  35266  subfacp1lem2a  35914  subfacp1lem2b  35915  subfacp1lem5  35918  ismtyres  38710  diaclN  42075  dia1elN  42079  diaintclN  42083  docaclN  42149  dibintclN  42192  cantnf2  44285  permaxun  45953  permac8prim  45956  nregmodellem  45958  sge0f1o  47336  f1oresf1o  48304  grimuhgr  48929  uhgrimisgrgric  48973