Theorem f1fn 5600

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 5372  ⟶wf 5373  –1-1→wf1 5374

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f 5381  df-f1 5382

This theorem is used by:  f1fun  5601  f1rel  5602  f1dm  5603  f1ssr  5605  f1f1orn  5650  f1elima  5979  f1eqcocnv  5997  f1oiso  6032  phplem4dom  7163  f1finf1o  7264  updjudhcoinlf  7420  updjudhcoinrg  7421  updjud  7422  fihashf1rn  11227  hashf1lem1  11285  hashf1  11287  kerf1ghm  14077  domomsubct  17031