Theorem f1fn 6102

Description: A one-to-one mapping is a function on its domain. (Contributed by NM, 8-Mar-2014.)

Assertion

Ref	Expression
f1fn	⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)

Proof of Theorem f1fn

Step	Hyp	Ref	Expression
1		f1f 6101	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		ffn 6045	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 5883  ⟶wf 5884  –1-1→wf1 5885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-f 5892  df-f1 5893

This theorem is referenced by:  f1fun  6103  f1rel  6104  f1dm  6105  f1ssr  6107  f1f1orn  6148  f1elima  6520  f1eqcocnv  6556  domunsncan  8060  marypha2  8345  infdifsn  8554  acndom  8874  dfac12lem2  8966  ackbij1  9060  fin23lem32  9166  fin1a2lem5  9226  fin1a2lem6  9227  pwfseqlem1  9480  hashf1lem1  13239  hashf1  13241  odf1o2  17988  kerf1hrm  18743  frlmlbs  20136  f1lindf  20161  2ndcdisj  21259  qtopf1  21619  clwlkclwwlklem2  26901  erdszelem10  31182  dihfn  36557  dihcl  36559  dih1dimatlem  36618  dochocss  36655