Theorem f1fn 6737

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

Syntax hints:   → wi 4   Fn wfn 6493  –1-1→wf1 6495

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 6502  df-f1 6503

This theorem is referenced by:  f1fun  6738  f1rel  6739  f1dm  6740  f1ssr  6742  f1f1orn  6791  f1elima  7218  f1eqcocnv  7256  domunsncan  9015  f1domfi2  9116  sbthfilem  9132  fodomfir  9238  marypha2  9352  infdifsn  9578  acndom  9973  dfac12lem2  10067  ackbij1  10159  fin23lem32  10266  fin1a2lem5  10326  fin1a2lem6  10327  pwfseqlem1  10581  hashf1lem1  14417  hashf1  14419  kerf1ghm  19222  odf1o2  19548  frlmlbs  21777  f1lindf  21802  2ndcdisj  23421  qtopf1  23781  clwlkclwwlklem2  30070  f1rnen  32701  fineqvinfep  35269  erdszelem10  35382  pibt2  37733  dihfn  41714  dihcl  41716  dih1dimatlem  41775  dochocss  41812  onsucf1o  43700  cantnfub  43749  cantnfub2  43750  gricushgr  48393  grtrimap  48424