Theorem f1ofun 5428

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

Syntax hints:   → wi 4  Fun wfun 5176   Fn wfn 5177  –1-1-onto→wf1o 5181

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

This theorem depends on definitions:  df-bi 116  df-fn 5185  df-f 5186  df-f1 5187  df-f1o 5189

This theorem is referenced by:  f1orel  5429  f1oresrab  5644  isose  5783  f1opw  6039  xpcomco  6783  fiintim  6885  f1dmvrnfibi  6900  caseinl  7047  caseinr  7048  ctssdccl  7067  ctssdclemr  7068  fihasheqf1oi  10690  fisumss  11319  ennnfonelemex  12284  ennnfonelemf1  12288  hmeontr  12854