Theorem f1ofun 5585

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

Syntax hints:   → wi 4  Fun wfun 5320   Fn wfn 5321  –1-1-onto→wf1o 5325

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 5329  df-f 5330  df-f1 5331  df-f1o 5333

This theorem is referenced by:  f1orel  5586  f1oresrab  5812  isose  5962  f1opw  6230  xpcomco  7010  fiintim  7123  f1dmvrnfibi  7143  caseinl  7290  caseinr  7291  ctssdccl  7310  ctssdclemr  7311  fihasheqf1oi  11050  fisumss  11955  ennnfonelemex  13037  ennnfonelemf1  13041  hmeontr  15040