Theorem f1fn 6775

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

Syntax hints:   → wi 4   Fn wfn 6531  –1-1→wf1 6533

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 210  df-an 401  df-f 6540  df-f1 6541

This theorem is referenced by:  f1fun  6776  f1funOLD  6777  f1relOLD  6779  f1dm  6780  f1ssr  6782  f1f1orn  6832  f1elima  7261  f1eqcocnv  7299  domunsncan  9061  f1domfi2  9162  sbthfilem  9178  fodomfir  9283  marypha2  9395  infdifsn  9622  acndom  10031  dfac12lem2  10124  ackbij1  10216  fin23lem32  10323  fin1a2lem5  10383  fin1a2lem6  10384  pwfseqlem1  10638  hashf1lem1  14488  hashf1  14490  kerf1ghm  19312  odf1o2  19638  frlmlbs  21947  f1lindf  21972  2ndcdisj  23613  qtopf1  23973  clwlkclwwlklem2  30351  f1rnen  32973  fineqvinfep  35538  vonf1wev  35592  erdszelem10  35692  pibt2  38063  dihfn  42042  dihcl  42044  dih1dimatlem  42103  dochocss  42140  onsucf1o  43999  cantnfub  44048  cantnfub2  44049  gricushgr  48682  grtrimap  48713