Theorem f1fn 5535

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

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

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

This theorem is referenced by:  f1fun  5536  f1rel  5537  f1dm  5538  f1ssr  5540  f1f1orn  5585  f1elima  5903  f1eqcocnv  5921  f1oiso  5956  phplem4dom  7031  f1finf1o  7125  updjudhcoinlf  7258  updjudhcoinrg  7259  updjud  7260  fihashf1rn  11022  kerf1ghm  13826  domomsubct  16426