Theorem f1fn 5595

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

Syntax hints:   → wi 4   Fn wfn 5367  ⟶wf 5368  –1-1→wf1 5369

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 5376  df-f1 5377

This theorem is referenced by:  f1fun  5596  f1rel  5597  f1dm  5598  f1ssr  5600  f1f1orn  5645  f1elima  5969  f1eqcocnv  5987  f1oiso  6022  phplem4dom  7153  f1finf1o  7254  updjudhcoinlf  7410  updjudhcoinrg  7411  updjud  7412  fihashf1rn  11205  hashf1lem1  11263  hashf1  11265  kerf1ghm  14054  domomsubct  16945