Theorem f1fn 6789

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

Syntax hints:   → wi 4   Fn wfn 6539  –1-1→wf1 6541

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 206  df-an 398  df-f 6548  df-f1 6549

This theorem is referenced by:  f1fun  6790  f1rel  6791  f1dm  6792  f1dmOLD  6793  f1ssr  6795  f1f1orn  6845  f1elima  7262  f1eqcocnv  7299  f1eqcocnvOLD  7300  domunsncan  9072  f1domfi2  9185  sbthfilem  9201  marypha2  9434  infdifsn  9652  acndom  10046  dfac12lem2  10139  ackbij1  10233  fin23lem32  10339  fin1a2lem5  10399  fin1a2lem6  10400  pwfseqlem1  10653  hashf1lem1  14415  hashf1lem1OLD  14416  hashf1  14418  odf1o2  19441  kerf1ghm  20282  frlmlbs  21352  f1lindf  21377  2ndcdisj  22960  qtopf1  23320  clwlkclwwlklem2  29253  f1rnen  31853  erdszelem10  34191  pibt2  36298  dihfn  40139  dihcl  40141  dih1dimatlem  40200  dochocss  40237  onsucf1o  42022  cantnfub  42071  cantnfub2  42072  isomushgr  46494