Theorem f1ofun 5641

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 5371   Fn wfn 5372  –1-1-onto→wf1o 5376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-fn 5380  df-f 5381  df-f1 5382  df-f1o 5384

This theorem is used by:  f1orel  5642  f1oresrab  5873  isose  6027  f1opw  6297  xpcomco  7124  fiintim  7238  f1dmvrnfibi  7258  caseinl  7432  caseinr  7433  ctssdccl  7452  ctssdclemr  7453  fihasheqf1oi  11241  fisumss  12177  ballotfilemrv  13314  ennnfonelemex  13356  ennnfonelemf1  13360  hmeontr  15466