Theorem f1fn 6805

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

Syntax hints:   → wi 4   Fn wfn 6556  –1-1→wf1 6558

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 6565  df-f1 6566

This theorem is referenced by:  f1fun  6806  f1rel  6807  f1dm  6808  f1ssr  6810  f1f1orn  6859  f1elima  7283  f1eqcocnv  7321  domunsncan  9112  f1domfi2  9222  sbthfilem  9238  fodomfir  9368  marypha2  9479  infdifsn  9697  acndom  10091  dfac12lem2  10185  ackbij1  10277  fin23lem32  10384  fin1a2lem5  10444  fin1a2lem6  10445  pwfseqlem1  10698  hashf1lem1  14494  hashf1  14496  kerf1ghm  19265  odf1o2  19591  frlmlbs  21817  f1lindf  21842  2ndcdisj  23464  qtopf1  23824  clwlkclwwlklem2  30019  f1rnen  32639  erdszelem10  35205  pibt2  37418  dihfn  41270  dihcl  41272  dih1dimatlem  41331  dochocss  41368  onsucf1o  43285  cantnfub  43334  cantnfub2  43335  gricushgr  47886  grtrimap  47915