Theorem f1fn 5482

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

Syntax hints:   → wi 4   Fn wfn 5265  ⟶wf 5266  –1-1→wf1 5267

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 5274  df-f1 5275

This theorem is referenced by:  f1fun  5483  f1rel  5484  f1dm  5485  f1ssr  5487  f1f1orn  5532  f1elima  5841  f1eqcocnv  5859  f1oiso  5894  phplem4dom  6958  f1finf1o  7048  updjudhcoinlf  7181  updjudhcoinrg  7182  updjud  7183  fihashf1rn  10931  kerf1ghm  13552  domomsubct  15871