Theorem f1fn 5477

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

Syntax hints:   → wi 4   Fn wfn 5263  ⟶wf 5264  –1-1→wf1 5265

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 5272  df-f1 5273

This theorem is referenced by:  f1fun  5478  f1rel  5479  f1dm  5480  f1ssr  5482  f1f1orn  5527  f1elima  5832  f1eqcocnv  5850  f1oiso  5885  phplem4dom  6941  f1finf1o  7031  updjudhcoinlf  7164  updjudhcoinrg  7165  updjud  7166  fihashf1rn  10914  kerf1ghm  13528  domomsubct  15802