Theorem f1ofun 6840

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

Syntax hints:   → wi 4  Fun wfun 6543   Fn wfn 6544  –1-1-onto→wf1o 6548

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 206  df-an 395  df-fn 6552  df-f 6553  df-f1 6554  df-f1o 6556

This theorem is referenced by:  f1orel  6841  f1oresrab  7136  fveqf1o  7311  isofrlem  7347  isofr  7349  isose  7350  f1opw  7677  xpcomco  9087  dif1en  9185  dif1enOLD  9187  f1opwfi  9382  inlresf  9939  inrresf  9941  djuun  9951  isercolllem2  15648  isercoll  15650  unbenlem  16880  gsumpropd2lem  18642  symgfixf1  19404  tgqtop  23660  hmeontr  23717  reghmph  23741  nrmhmph  23742  tgpconncompeqg  24060  cnheiborlem  24924  dfrelog  26544  dvloglem  26627  logf1o2  26629  axcontlem9  28855  axcontlem10  28856  padct  32583  symgcom  32896  cycpmconjvlem  32954  cycpmconjslem2  32968  madjusmdetlem2  33560  tpr2rico  33644  ballotlemrv  34270  reprpmtf1o  34389  hgt750lemg  34417  subfacp1lem2a  34921  subfacp1lem2b  34922  subfacp1lem5  34925  ismtyres  37412  diaclN  40653  dia1elN  40657  diaintclN  40661  docaclN  40727  dibintclN  40770  cantnf2  42896  sge0f1o  45908  f1oresf1o  46808  uspgrimprop  47357  grimuhgr  47362