Theorem f1fn 6772

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 6528  –1-1→wf1 6530

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f 6537  df-f1 6538

This theorem is used by:  f1fun  6773  f1funOLD  6774  f1relOLD  6776  f1dm  6777  f1ssr  6779  f1f1orn  6829  f1elima  7260  f1eqcocnv  7302  domunsncan  9075  f1domfi2  9176  sbthfilem  9192  fodomfir  9297  marypha2  9409  infdifsn  9636  acndom  10054  dfac12lem2  10147  ackbij1  10239  fin23lem32  10346  fin1a2lem5  10406  fin1a2lem6  10407  pwfseqlem1  10667  hashf1lem1  14520  hashf1  14522  kerf1ghm  19374  odf1o2  19700  frlmlbs  22010  f1lindf  22035  2ndcdisj  23682  qtopf1  24042  clwlkclwwlklem2  30470  f1rnen  33101  fineqvinfep  35651  vonf1wev  35705  erdszelem10  35779  pibt2  38171  dihfn  42141  dihcl  42143  dih1dimatlem  42202  dochocss  42239  onsucf1o  44113  cantnfub  44162  cantnfub2  44163  gricushgr  48833  grtrimap  48864