Theorem f1fn 6776

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

Syntax hints:   → wi 4   Fn wfn 6532  –1-1→wf1 6534

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 6541  df-f1 6542

This theorem is referenced by:  f1fun  6777  f1funOLD  6778  f1relOLD  6780  f1dm  6781  f1ssr  6783  f1f1orn  6833  f1elima  7262  f1eqcocnv  7300  domunsncan  9064  f1domfi2  9165  sbthfilem  9181  fodomfir  9286  marypha2  9398  infdifsn  9625  acndom  10034  dfac12lem2  10127  ackbij1  10219  fin23lem32  10327  fin1a2lem5  10387  fin1a2lem6  10388  pwfseqlem1  10642  hashf1lem1  14491  hashf1  14493  kerf1ghm  19316  odf1o2  19642  frlmlbs  21915  f1lindf  21940  2ndcdisj  23581  qtopf1  23941  clwlkclwwlklem2  30291  f1rnen  32913  fineqvinfep  35460  vonf1wev  35490  erdszelem10  35590  pibt2  37950  dihfn  41931  dihcl  41933  dih1dimatlem  41992  dochocss  42029  onsucf1o  43890  cantnfub  43939  cantnfub2  43940  gricushgr  48570  grtrimap  48601