Theorem f1fn 5575

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

Syntax hints:   → wi 4   Fn wfn 5347  ⟶wf 5348  –1-1→wf1 5349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-f 5356  df-f1 5357

This theorem is referenced by:  f1fun  5576  f1rel  5577  f1dm  5578  f1ssr  5580  f1f1orn  5625  f1elima  5946  f1eqcocnv  5964  f1oiso  5999  phplem4dom  7116  f1finf1o  7217  updjudhcoinlf  7371  updjudhcoinrg  7372  updjud  7373  fihashf1rn  11151  kerf1ghm  13991  domomsubct  16775