Theorem f1fn 6317

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 6316	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2	1	ffnd 6257	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 6096  –1-1→wf1 6098

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 199  df-an 386  df-f 6105  df-f1 6106

This theorem is referenced by:  f1fun  6318  f1rel  6319  f1dm  6320  f1ssr  6322  f1f1orn  6367  f1elima  6748  f1eqcocnv  6784  domunsncan  8302  marypha2  8587  infdifsn  8804  acndom  9160  dfac12lem2  9254  ackbij1  9348  fin23lem32  9454  fin1a2lem5  9514  fin1a2lem6  9515  pwfseqlem1  9768  hashf1lem1  13488  hashf1  13490  odf1o2  18301  kerf1hrm  19061  frlmlbs  20461  f1lindf  20486  2ndcdisj  21588  qtopf1  21948  clwlkclwwlklem2  27293  erdszelem10  31699  dihfn  37289  dihcl  37291  dih1dimatlem  37350  dochocss  37387  isomushgr  42496