Theorem f1ofun 5582

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

Syntax hints:   → wi 4  Fun wfun 5318   Fn wfn 5319  –1-1-onto→wf1o 5323

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 5327  df-f 5328  df-f1 5329  df-f1o 5331

This theorem is referenced by:  f1orel  5583  f1oresrab  5808  isose  5957  f1opw  6225  xpcomco  7005  fiintim  7118  f1dmvrnfibi  7137  caseinl  7284  caseinr  7285  ctssdccl  7304  ctssdclemr  7305  fihasheqf1oi  11042  fisumss  11946  ennnfonelemex  13028  ennnfonelemf1  13032  hmeontr  15030