Theorem f1ofun 5579

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

Syntax hints:   → wi 4  Fun wfun 5315   Fn wfn 5316  –1-1-onto→wf1o 5320

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 5324  df-f 5325  df-f1 5326  df-f1o 5328

This theorem is referenced by:  f1orel  5580  f1oresrab  5805  isose  5954  f1opw  6222  xpcomco  6998  fiintim  7109  f1dmvrnfibi  7127  caseinl  7274  caseinr  7275  ctssdccl  7294  ctssdclemr  7295  fihasheqf1oi  11026  fisumss  11924  ennnfonelemex  13006  ennnfonelemf1  13010  hmeontr  15008