Theorem f1fn 6731

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 6730	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2	1	ffnd 6663	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 6487  –1-1→wf1 6489

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 207  df-an 396  df-f 6496  df-f1 6497

This theorem is referenced by:  f1fun  6732  f1rel  6733  f1dm  6734  f1ssr  6736  f1f1orn  6785  f1elima  7209  f1eqcocnv  7247  domunsncan  9005  f1domfi2  9106  sbthfilem  9122  fodomfir  9228  marypha2  9342  infdifsn  9566  acndom  9961  dfac12lem2  10055  ackbij1  10147  fin23lem32  10254  fin1a2lem5  10314  fin1a2lem6  10315  pwfseqlem1  10569  hashf1lem1  14378  hashf1  14380  kerf1ghm  19176  odf1o2  19502  frlmlbs  21752  f1lindf  21777  2ndcdisj  23400  qtopf1  23760  clwlkclwwlklem2  30075  f1rnen  32706  fineqvinfep  35281  erdszelem10  35394  pibt2  37622  dihfn  41528  dihcl  41530  dih1dimatlem  41589  dochocss  41626  onsucf1o  43514  cantnfub  43563  cantnfub2  43564  gricushgr  48163  grtrimap  48194