Theorem f1ofun 5503

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

Syntax hints:   → wi 4  Fun wfun 5249   Fn wfn 5250  –1-1-onto→wf1o 5254

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 5258  df-f 5259  df-f1 5260  df-f1o 5262

This theorem is referenced by:  f1orel  5504  f1oresrab  5724  isose  5865  f1opw  6127  xpcomco  6882  fiintim  6987  f1dmvrnfibi  7005  caseinl  7152  caseinr  7153  ctssdccl  7172  ctssdclemr  7173  fihasheqf1oi  10861  fisumss  11538  ennnfonelemex  12574  ennnfonelemf1  12578  hmeontr  14492