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  18762  symgfixf1  19532  tgqtop  23899  hmeontr  23956  reghmph  23980  nrmhmph  23981  tgpconncompeqg  24299  cnheiborlem  25143  dfrelog  26760  dvloglem  26843  logf1o2  26845  axcontlem9  29352  axcontlem10  29353  padct  33093  symgcom  33427  cycpmconjvlem  33485  cycpmconjslem2  33499  madjusmdetlem2  34242  tpr2rico  34326  ballotlemrv  34934  reprpmtf1o  35037  hgt750lemg  35065  subfacp1lem2a  35685  subfacp1lem2b  35686  subfacp1lem5  35689  ismtyres  38492  diaclN  41857  dia1elN  41861  diaintclN  41865  docaclN  41931  dibintclN  41974  cantnf2  44085  permaxun  45753  permac8prim  45756  nregmodellem  45758  sge0f1o  47129  f1oresf1o  48060  grimuhgr  48685  uhgrimisgrgric  48729