Theorem f1fn 5553

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

Syntax hints:   → wi 4   Fn wfn 5328  ⟶wf 5329  –1-1→wf1 5330

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 5337  df-f1 5338

This theorem is referenced by:  f1fun  5554  f1rel  5555  f1dm  5556  f1ssr  5558  f1f1orn  5603  f1elima  5924  f1eqcocnv  5942  f1oiso  5977  phplem4dom  7091  f1finf1o  7189  updjudhcoinlf  7322  updjudhcoinrg  7323  updjud  7324  fihashf1rn  11096  kerf1ghm  13924  domomsubct  16706