Theorem f1fn 5541

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

Syntax hints:   → wi 4   Fn wfn 5319  ⟶wf 5320  –1-1→wf1 5321

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 5328  df-f1 5329

This theorem is referenced by:  f1fun  5542  f1rel  5543  f1dm  5544  f1ssr  5546  f1f1orn  5591  f1elima  5909  f1eqcocnv  5927  f1oiso  5962  phplem4dom  7043  f1finf1o  7137  updjudhcoinlf  7270  updjudhcoinrg  7271  updjud  7272  fihashf1rn  11040  kerf1ghm  13851  domomsubct  16538