Theorem f1ofun 5594

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

Syntax hints:   → wi 4  Fun wfun 5327   Fn wfn 5328  –1-1-onto→wf1o 5332

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 5336  df-f 5337  df-f1 5338  df-f1o 5340

This theorem is referenced by:  f1orel  5595  f1oresrab  5820  isose  5972  f1opw  6240  xpcomco  7053  fiintim  7166  f1dmvrnfibi  7186  caseinl  7333  caseinr  7334  ctssdccl  7353  ctssdclemr  7354  fihasheqf1oi  11093  fisumss  12014  ennnfonelemex  13096  ennnfonelemf1  13100  hmeontr  15104