Theorem f1ofun 6833

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

Syntax hints:   → wi 4  Fun wfun 6535   Fn wfn 6536  –1-1-onto→wf1o 6540

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 398  df-fn 6544  df-f 6545  df-f1 6546  df-f1o 6548

This theorem is referenced by:  f1orel  6834  f1oresrab  7122  fveqf1o  7298  isofrlem  7334  isofr  7336  isose  7337  f1opw  7659  xpcomco  9059  dif1en  9157  dif1enOLD  9159  f1opwfi  9353  inlresf  9906  inrresf  9908  djuun  9918  isercolllem2  15609  isercoll  15611  unbenlem  16838  gsumpropd2lem  18595  symgfixf1  19300  tgqtop  23208  hmeontr  23265  reghmph  23289  nrmhmph  23290  tgpconncompeqg  23608  cnheiborlem  24462  dfrelog  26066  dvloglem  26148  logf1o2  26150  axcontlem9  28220  axcontlem10  28221  padct  31932  symgcom  32232  cycpmconjvlem  32288  cycpmconjslem2  32302  madjusmdetlem2  32797  tpr2rico  32881  ballotlemrv  33507  reprpmtf1o  33627  hgt750lemg  33655  subfacp1lem2a  34160  subfacp1lem2b  34161  subfacp1lem5  34164  ismtyres  36665  diaclN  39910  dia1elN  39914  diaintclN  39918  docaclN  39984  dibintclN  40027  cantnf2  42061  sge0f1o  45085  f1oresf1o  45985