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  7431  caseinr  7432  ctssdccl  7451  ctssdclemr  7452  fihasheqf1oi  11228  fisumss  12161  ballotfilemrv  13265  ennnfonelemex  13307  ennnfonelemf1  13311  hmeontr  15416