Theorem f1ofun 5509

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

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

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 5262  df-f 5263  df-f1 5264  df-f1o 5266

This theorem is referenced by:  f1orel  5510  f1oresrab  5730  isose  5871  f1opw  6134  xpcomco  6894  fiintim  7001  f1dmvrnfibi  7019  caseinl  7166  caseinr  7167  ctssdccl  7186  ctssdclemr  7187  fihasheqf1oi  10896  fisumss  11574  ennnfonelemex  12656  ennnfonelemf1  12660  hmeontr  14633