Theorem f1fn 6797

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

Syntax hints:   → wi 4   Fn wfn 6546  –1-1→wf1 6548

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 395  df-f 6555  df-f1 6556

This theorem is referenced by:  f1fun  6798  f1rel  6799  f1dm  6800  f1dmOLD  6801  f1ssr  6803  f1f1orn  6853  f1elima  7277  f1eqcocnv  7314  f1eqcocnvOLD  7315  domunsncan  9101  f1domfi2  9214  sbthfilem  9230  marypha2  9468  infdifsn  9686  acndom  10080  dfac12lem2  10173  ackbij1  10267  fin23lem32  10373  fin1a2lem5  10433  fin1a2lem6  10434  pwfseqlem1  10687  hashf1lem1  14453  hashf1lem1OLD  14454  hashf1  14456  kerf1ghm  19206  odf1o2  19533  frlmlbs  21736  f1lindf  21761  2ndcdisj  23378  qtopf1  23738  clwlkclwwlklem2  29828  f1rnen  32432  erdszelem10  34815  pibt2  36901  dihfn  40745  dihcl  40747  dih1dimatlem  40806  dochocss  40843  onsucf1o  42704  cantnfub  42753  cantnfub2  42754  gricushgr  47234