Theorem f1ofun 5618

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

Syntax hints:   → wi 4  Fun wfun 5348   Fn wfn 5349  –1-1-onto→wf1o 5353

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 5357  df-f 5358  df-f1 5359  df-f1o 5361

This theorem is referenced by:  f1orel  5619  f1oresrab  5844  isose  5996  f1opw  6264  xpcomco  7079  fiintim  7193  f1dmvrnfibi  7213  caseinl  7384  caseinr  7385  ctssdccl  7404  ctssdclemr  7405  fihasheqf1oi  11154  fisumss  12082  ennnfonelemex  13182  ennnfonelemf1  13186  hmeontr  15195