Theorem f1ofun 6826

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

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

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

This theorem is used by:  f1orel  6827  f1oresrab  7128  fveqf1o  7310  isofrlem  7348  isofr  7350  isose  7351  f1opw  7677  xpcomco  9089  dif1en  9180  f1opwfi  9348  inlresf  9998  inrresf  10000  djuun  10010  isercolllem2  15838  isercoll  15840  unbenlem  17091  gsumpropd2lem  18873  symgfixf1  19656  tgqtop  24036  hmeontr  24093  reghmph  24117  nrmhmph  24118  tgpconncompeqg  24436  cnheiborlem  25280  dfrelog  26898  dvloglem  26981  logf1o2  26983  axcontlem9  29555  axcontlem10  29556  padct  33357  symgcom  33690  cycpmconjvlem  33748  cycpmconjslem2  33762  madjusmdetlem2  34506  tpr2rico  34590  ballotlemrv  35198  reprpmtf1o  35301  hgt750lemg  35329  onprcf1of1orbd  35973  subfacp1lem2a  36031  subfacp1lem2b  36032  subfacp1lem5  36035  ismtyres  38835  diaclN  42200  dia1elN  42204  diaintclN  42208  docaclN  42274  dibintclN  42317  cantnf2  44420  permaxun  46094  permac8prim  46097  nregmodellem  46099  hfstructcan  46124  sge0f1o  47485  f1oresf1o  48453  grimuhgr  49078  uhgrimisgrgric  49122