Theorem f1fn 6140

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

Syntax hints:   → wi 4   Fn wfn 5921  ⟶wf 5922  –1-1→wf1 5923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 385  df-f 5930  df-f1 5931

This theorem is referenced by:  f1fun  6141  f1rel  6142  f1dm  6143  f1ssr  6145  f1f1orn  6186  f1elima  6560  f1eqcocnv  6596  domunsncan  8101  marypha2  8386  infdifsn  8592  acndom  8912  dfac12lem2  9004  ackbij1  9098  fin23lem32  9204  fin1a2lem5  9264  fin1a2lem6  9265  pwfseqlem1  9518  hashf1lem1  13277  hashf1  13279  odf1o2  18034  kerf1hrm  18791  frlmlbs  20184  f1lindf  20209  2ndcdisj  21307  qtopf1  21667  clwlkclwwlklem2  26966  erdszelem10  31308  dihfn  36874  dihcl  36876  dih1dimatlem  36935  dochocss  36972