Theorem f1fn 6809

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 6561  ⟶1-1wf1 6563

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 6570  df-f1 6571

This theorem is used by:  f1fun  6810  f1funOLD  6811  f1relOLD  6813  f1dm  6814  f1ssr  6816  f1f1orn  6866  f1elima  7298  f1eqcocnv  7340  domunsncan  9134  f1domfi2  9235  sbthfilem  9251  fodomfir  9357  marypha2  9468  infdifsn  9695  acndom  10169  dfac12lem2  10262  ackbij1  10354  fin23lem32  10461  fin1a2lem5  10521  fin1a2lem6  10522  pwfseqlem1  10782  hashf1lem1  14641  hashf1  14643  kerf1ghm  19511  odf1o2  19838  frlmlbs  22158  f1lindf  22183  2ndcdisj  23830  qtopf1  24190  clwlkclwwlklem2  30648  f1rnen  33320  fineqvinfep  35934  vonf1wev  36077  erdszelem10  36173  pibt2  38608  dihfn  42591  dihcl  42593  dih1dimatlem  42652  dochocss  42689  onsucf1o  44535  cantnfub  44584  cantnfub2  44585  gricushgr  49288  grtrimap  49319