Theorem f1ofun 5455

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

Syntax hints:   → wi 4  Fun wfun 5202   Fn wfn 5203  –1-1-onto→wf1o 5207

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 5211  df-f 5212  df-f1 5213  df-f1o 5215

This theorem is referenced by:  f1orel  5456  f1oresrab  5673  isose  5812  f1opw  6068  xpcomco  6816  fiintim  6918  f1dmvrnfibi  6933  caseinl  7080  caseinr  7081  ctssdccl  7100  ctssdclemr  7101  fihasheqf1oi  10735  fisumss  11368  ennnfonelemex  12382  ennnfonelemf1  12386  hmeontr  13384