Theorem f1fn 5468

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

Syntax hints:   → wi 4   Fn wfn 5254  ⟶wf 5255  –1-1→wf1 5256

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 5263  df-f1 5264

This theorem is referenced by:  f1fun  5469  f1rel  5470  f1dm  5471  f1ssr  5473  f1f1orn  5518  f1elima  5823  f1eqcocnv  5841  f1oiso  5876  phplem4dom  6932  f1finf1o  7022  updjudhcoinlf  7155  updjudhcoinrg  7156  updjud  7157  fihashf1rn  10897  kerf1ghm  13480  domomsubct  15732