Theorem f1fn 6739

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

Syntax hints:   → wi 4   Fn wfn 6494  –1-1→wf1 6496

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 6503  df-f1 6504

This theorem is referenced by:  f1fun  6740  f1rel  6741  f1dm  6742  f1ssr  6744  f1f1orn  6793  f1elima  7220  f1eqcocnv  7258  domunsncan  9018  f1domfi2  9123  sbthfilem  9139  fodomfir  9255  marypha2  9366  infdifsn  9586  acndom  9980  dfac12lem2  10074  ackbij1  10166  fin23lem32  10273  fin1a2lem5  10333  fin1a2lem6  10334  pwfseqlem1  10587  hashf1lem1  14396  hashf1  14398  kerf1ghm  19155  odf1o2  19479  frlmlbs  21682  f1lindf  21707  2ndcdisj  23319  qtopf1  23679  clwlkclwwlklem2  29902  f1rnen  32526  erdszelem10  35160  pibt2  37378  dihfn  41235  dihcl  41237  dih1dimatlem  41296  dochocss  41333  onsucf1o  43234  cantnfub  43283  cantnfub2  43284  gricushgr  47890  grtrimap  47920