Theorem f1ofun 5531

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

Syntax hints:   → wi 4  Fun wfun 5270   Fn wfn 5271  –1-1-onto→wf1o 5275

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 5279  df-f 5280  df-f1 5281  df-f1o 5283

This theorem is referenced by:  f1orel  5532  f1oresrab  5752  isose  5897  f1opw  6160  xpcomco  6928  fiintim  7035  f1dmvrnfibi  7053  caseinl  7200  caseinr  7201  ctssdccl  7220  ctssdclemr  7221  fihasheqf1oi  10939  fisumss  11747  ennnfonelemex  12829  ennnfonelemf1  12833  hmeontr  14829