Theorem f1ofun 5550

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

Syntax hints:   → wi 4  Fun wfun 5288   Fn wfn 5289  –1-1-onto→wf1o 5293

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 5297  df-f 5298  df-f1 5299  df-f1o 5301

This theorem is referenced by:  f1orel  5551  f1oresrab  5773  isose  5918  f1opw  6183  xpcomco  6953  fiintim  7061  f1dmvrnfibi  7079  caseinl  7226  caseinr  7227  ctssdccl  7246  ctssdclemr  7247  fihasheqf1oi  10976  fisumss  11869  ennnfonelemex  12951  ennnfonelemf1  12955  hmeontr  14952