Theorem f1ofun 5639

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

Syntax hints:   → wi 4  Fun wfun 5369   Fn wfn 5370  –1-1-onto→wf1o 5374

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 5378  df-f 5379  df-f1 5380  df-f1o 5382

This theorem is referenced by:  f1orel  5640  f1oresrab  5867  isose  6021  f1opw  6291  xpcomco  7118  fiintim  7232  f1dmvrnfibi  7252  caseinl  7425  caseinr  7426  ctssdccl  7445  ctssdclemr  7446  fihasheqf1oi  11209  fisumss  12142  ballotfilemrv  13246  ennnfonelemex  13288  ennnfonelemf1  13292  hmeontr  15397