Theorem f1ofun 5434

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

Syntax hints:   → wi 4  Fun wfun 5182   Fn wfn 5183  –1-1-onto→wf1o 5187

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 5191  df-f 5192  df-f1 5193  df-f1o 5195

This theorem is referenced by:  f1orel  5435  f1oresrab  5650  isose  5789  f1opw  6045  xpcomco  6792  fiintim  6894  f1dmvrnfibi  6909  caseinl  7056  caseinr  7057  ctssdccl  7076  ctssdclemr  7077  fihasheqf1oi  10701  fisumss  11333  ennnfonelemex  12347  ennnfonelemf1  12351  hmeontr  12953