Theorem f1ofun 5615

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

Syntax hints:   → wi 4  Fun wfun 5345   Fn wfn 5346  –1-1-onto→wf1o 5350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-fn 5354  df-f 5355  df-f1 5356  df-f1o 5358

This theorem is referenced by:  f1orel  5616  f1oresrab  5841  isose  5993  f1opw  6261  xpcomco  7076  fiintim  7190  f1dmvrnfibi  7210  caseinl  7381  caseinr  7382  ctssdccl  7401  ctssdclemr  7402  fihasheqf1oi  11148  fisumss  12074  ennnfonelemex  13157  ennnfonelemf1  13161  hmeontr  15170