Theorem f1fn 5532

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

Syntax hints:   → wi 4   Fn wfn 5312  ⟶wf 5313  –1-1→wf1 5314

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 5321  df-f1 5322

This theorem is referenced by:  f1fun  5533  f1rel  5534  f1dm  5535  f1ssr  5537  f1f1orn  5582  f1elima  5896  f1eqcocnv  5914  f1oiso  5949  phplem4dom  7019  f1finf1o  7110  updjudhcoinlf  7243  updjudhcoinrg  7244  updjud  7245  fihashf1rn  11005  kerf1ghm  13806  domomsubct  16326