Theorem f1fn 6576

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

Syntax hints:   → wi 4   Fn wfn 6335  –1-1→wf1 6337

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 210  df-an 400  df-f 6344  df-f1 6345

This theorem is referenced by:  f1fun  6577  f1rel  6578  f1dm  6579  f1dmOLD  6580  f1ssr  6582  f1f1orn  6630  f1elima  7033  f1eqcocnv  7069  f1eqcocnvOLD  7070  domunsncan  8667  marypha2  8977  infdifsn  9194  acndom  9552  dfac12lem2  9645  ackbij1  9739  fin23lem32  9845  fin1a2lem5  9905  fin1a2lem6  9906  pwfseqlem1  10159  hashf1lem1  13907  hashf1lem1OLD  13908  hashf1  13910  odf1o2  18817  kerf1ghm  19618  frlmlbs  20614  f1lindf  20639  2ndcdisj  22208  qtopf1  22568  clwlkclwwlklem2  27937  f1rnen  30538  erdszelem10  32733  pibt2  35208  dihfn  38902  dihcl  38904  dih1dimatlem  38963  dochocss  39000  isomushgr  44804