Theorem f1ofun 5576

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

Syntax hints:   → wi 4  Fun wfun 5312   Fn wfn 5313  –1-1-onto→wf1o 5317

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 5321  df-f 5322  df-f1 5323  df-f1o 5325

This theorem is referenced by:  f1orel  5577  f1oresrab  5802  isose  5951  f1opw  6219  xpcomco  6993  fiintim  7101  f1dmvrnfibi  7119  caseinl  7266  caseinr  7267  ctssdccl  7286  ctssdclemr  7287  fihasheqf1oi  11017  fisumss  11911  ennnfonelemex  12993  ennnfonelemf1  12997  hmeontr  14995