Theorem f1fn 6761

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

Syntax hints:   → wi 4   Fn wfn 6516  –1-1→wf1 6518

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 209  df-an 400  df-f 6525  df-f1 6526

This theorem is referenced by:  f1fun  6762  f1funOLD  6763  f1relOLD  6765  f1dm  6766  f1ssr  6768  f1f1orn  6818  f1elima  7247  f1eqcocnv  7285  domunsncan  9049  f1domfi2  9150  sbthfilem  9166  fodomfir  9272  marypha2  9385  infdifsn  9612  acndom  10007  dfac12lem2  10101  ackbij1  10193  fin23lem32  10301  fin1a2lem5  10361  fin1a2lem6  10362  pwfseqlem1  10616  hashf1lem1  14468  hashf1  14470  kerf1ghm  19287  odf1o2  19613  frlmlbs  21846  f1lindf  21871  2ndcdisj  23513  qtopf1  23873  clwlkclwwlklem2  30199  f1rnen  32827  fineqvinfep  35418  vonf1wev  35448  erdszelem10  35547  pibt2  37908  dihfn  41889  dihcl  41891  dih1dimatlem  41950  dochocss  41987  onsucf1o  43846  cantnfub  43895  cantnfub2  43896  gricushgr  48536  grtrimap  48567