Theorem f1fn 6780

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

Syntax hints:   → wi 4   Fn wfn 6531  –1-1→wf1 6533

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 6540  df-f1 6541

This theorem is referenced by:  f1fun  6781  f1rel  6782  f1dm  6783  f1ssr  6785  f1f1orn  6834  f1elima  7261  f1eqcocnv  7299  domunsncan  9091  f1domfi2  9201  sbthfilem  9217  fodomfir  9345  marypha2  9456  infdifsn  9676  acndom  10070  dfac12lem2  10164  ackbij1  10256  fin23lem32  10363  fin1a2lem5  10423  fin1a2lem6  10424  pwfseqlem1  10677  hashf1lem1  14478  hashf1  14480  kerf1ghm  19235  odf1o2  19559  frlmlbs  21762  f1lindf  21787  2ndcdisj  23399  qtopf1  23759  clwlkclwwlklem2  29986  f1rnen  32612  erdszelem10  35227  pibt2  37440  dihfn  41292  dihcl  41294  dih1dimatlem  41353  dochocss  41390  onsucf1o  43271  cantnfub  43320  cantnfub2  43321  gricushgr  47910  grtrimap  47940