Theorem f1fn 5580

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

Syntax hints:   → wi 4   Fn wfn 5352  ⟶wf 5353  –1-1→wf1 5354

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 5361  df-f1 5362

This theorem is referenced by:  f1fun  5581  f1rel  5582  f1dm  5583  f1ssr  5585  f1f1orn  5630  f1elima  5952  f1eqcocnv  5970  f1oiso  6005  phplem4dom  7129  f1finf1o  7230  updjudhcoinlf  7384  updjudhcoinrg  7385  updjud  7386  fihashf1rn  11176  kerf1ghm  14027  domomsubct  16901