Theorem f1fn 5495

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

Syntax hints:   → wi 4   Fn wfn 5275  ⟶wf 5276  –1-1→wf1 5277

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 5284  df-f1 5285

This theorem is referenced by:  f1fun  5496  f1rel  5497  f1dm  5498  f1ssr  5500  f1f1orn  5545  f1elima  5855  f1eqcocnv  5873  f1oiso  5908  phplem4dom  6974  f1finf1o  7064  updjudhcoinlf  7197  updjudhcoinrg  7198  updjud  7199  fihashf1rn  10955  kerf1ghm  13685  domomsubct  16079