Theorem f1ofun 5644

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 5374   Fn wfn 5375  –1-1-onto→wf1o 5379

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 5383  df-f 5384  df-f1 5385  df-f1o 5387

This theorem is used by:  f1orel  5645  f1oresrab  5876  isose  6030  f1opw  6300  xpcomco  7129  fiintim  7243  f1dmvrnfibi  7263  caseinl  7438  caseinr  7439  ctssdccl  7458  ctssdclemr  7459  fihasheqf1oi  11249  fisumss  12185  ballotfilemrv  13322  ennnfonelemex  13364  ennnfonelemf1  13368  hmeontr  15551