Theorem f1fn 6015

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 6014	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		ffn 5958	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 5799  ⟶wf 5800  –1-1→wf1 5801

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 196  df-an 385  df-f 5808  df-f1 5809

This theorem is referenced by:  f1fun  6016  f1rel  6017  f1dm  6018  f1ssr  6020  f1f1orn  6061  f1elima  6421  f1eqcocnv  6456  domunsncan  7945  marypha2  8228  infdifsn  8437  acndom  8757  dfac12lem2  8849  ackbij1  8943  fin23lem32  9049  fin1a2lem5  9109  fin1a2lem6  9110  pwfseqlem1  9359  hashf1lem1  13096  hashf1  13098  odf1o2  17811  kerf1hrm  18566  frlmlbs  19955  f1lindf  19980  2ndcdisj  21069  qtopf1  21429  usgraedgrn  25910  usgfidegfi  26437  erdszelem10  30436  dihfn  35575  dihcl  35577  dih1dimatlem  35636  dochocss  35673  clwlkclwwlklem2  41209