Theorem f1fn 5544

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

Syntax hints:   → wi 4   Fn wfn 5321  ⟶wf 5322  –1-1→wf1 5323

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 5330  df-f1 5331

This theorem is referenced by:  f1fun  5545  f1rel  5546  f1dm  5547  f1ssr  5549  f1f1orn  5594  f1elima  5913  f1eqcocnv  5931  f1oiso  5966  phplem4dom  7047  f1finf1o  7145  updjudhcoinlf  7278  updjudhcoinrg  7279  updjud  7280  fihashf1rn  11049  kerf1ghm  13860  domomsubct  16602