Theorem f1fn 6715

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

Syntax hints:   → wi 4   Fn wfn 6471  –1-1→wf1 6473

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 6480  df-f1 6481

This theorem is referenced by:  f1fun  6716  f1rel  6717  f1dm  6718  f1ssr  6720  f1f1orn  6769  f1elima  7192  f1eqcocnv  7230  domunsncan  8985  f1domfi2  9086  sbthfilem  9102  fodomfir  9207  marypha2  9318  infdifsn  9542  acndom  9937  dfac12lem2  10031  ackbij1  10123  fin23lem32  10230  fin1a2lem5  10290  fin1a2lem6  10291  pwfseqlem1  10544  hashf1lem1  14357  hashf1  14359  kerf1ghm  19154  odf1o2  19480  frlmlbs  21729  f1lindf  21754  2ndcdisj  23366  qtopf1  23726  clwlkclwwlklem2  29972  f1rnen  32602  erdszelem10  35236  pibt2  37451  dihfn  41307  dihcl  41309  dih1dimatlem  41368  dochocss  41405  onsucf1o  43305  cantnfub  43354  cantnfub2  43355  gricushgr  47948  grtrimap  47979