Theorem f1fn 6579

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

Syntax hints:   → wi 4   Fn wfn 6353  –1-1→wf1 6355

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 209  df-an 399  df-f 6362  df-f1 6363

This theorem is referenced by:  f1fun  6580  f1rel  6581  f1dm  6582  f1ssr  6584  f1f1orn  6629  f1elima  7024  f1eqcocnv  7060  domunsncan  8620  marypha2  8906  infdifsn  9123  acndom  9480  dfac12lem2  9573  ackbij1  9663  fin23lem32  9769  fin1a2lem5  9829  fin1a2lem6  9830  pwfseqlem1  10083  hashf1lem1  13816  hashf1  13818  odf1o2  18701  kerf1ghm  19500  kerf1hrmOLD  19501  frlmlbs  20944  f1lindf  20969  2ndcdisj  22067  qtopf1  22427  clwlkclwwlklem2  27781  f1rnen  30377  erdszelem10  32451  pibt2  34702  dihfn  38408  dihcl  38410  dih1dimatlem  38469  dochocss  38506  isomushgr  43998