Theorem f1fn 6655

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

Syntax hints:   → wi 4   Fn wfn 6413  –1-1→wf1 6415

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 206  df-an 396  df-f 6422  df-f1 6423

This theorem is referenced by:  f1fun  6656  f1rel  6657  f1dm  6658  f1dmOLD  6659  f1ssr  6661  f1f1orn  6711  f1elima  7117  f1eqcocnv  7153  f1eqcocnvOLD  7154  domunsncan  8812  sbthfilem  8941  marypha2  9128  infdifsn  9345  acndom  9738  dfac12lem2  9831  ackbij1  9925  fin23lem32  10031  fin1a2lem5  10091  fin1a2lem6  10092  pwfseqlem1  10345  hashf1lem1  14096  hashf1lem1OLD  14097  hashf1  14099  odf1o2  19093  kerf1ghm  19902  frlmlbs  20914  f1lindf  20939  2ndcdisj  22515  qtopf1  22875  clwlkclwwlklem2  28265  f1rnen  30865  erdszelem10  33062  pibt2  35515  dihfn  39209  dihcl  39211  dih1dimatlem  39270  dochocss  39307  isomushgr  45166