Theorem f1fn 6731

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

Syntax hints:   → wi 4   Fn wfn 6487  –1-1→wf1 6489

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 207  df-an 396  df-f 6496  df-f1 6497

This theorem is referenced by:  f1fun  6732  f1rel  6733  f1dm  6734  f1ssr  6736  f1f1orn  6785  f1elima  7211  f1eqcocnv  7249  domunsncan  9008  f1domfi2  9109  sbthfilem  9125  fodomfir  9231  marypha2  9345  infdifsn  9569  acndom  9964  dfac12lem2  10058  ackbij1  10150  fin23lem32  10257  fin1a2lem5  10317  fin1a2lem6  10318  pwfseqlem1  10572  hashf1lem1  14408  hashf1  14410  kerf1ghm  19213  odf1o2  19539  frlmlbs  21787  f1lindf  21812  2ndcdisj  23431  qtopf1  23791  clwlkclwwlklem2  30085  f1rnen  32716  fineqvinfep  35285  erdszelem10  35398  pibt2  37747  dihfn  41728  dihcl  41730  dih1dimatlem  41789  dochocss  41826  onsucf1o  43718  cantnfub  43767  cantnfub2  43768  gricushgr  48405  grtrimap  48436