Theorem f1fn 6806

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

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

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 6567  df-f1 6568

This theorem is referenced by:  f1fun  6807  f1rel  6808  f1dm  6809  f1ssr  6811  f1f1orn  6860  f1elima  7283  f1eqcocnv  7321  domunsncan  9111  f1domfi2  9220  sbthfilem  9236  fodomfir  9366  marypha2  9477  infdifsn  9695  acndom  10089  dfac12lem2  10183  ackbij1  10275  fin23lem32  10382  fin1a2lem5  10442  fin1a2lem6  10443  pwfseqlem1  10696  hashf1lem1  14491  hashf1  14493  kerf1ghm  19278  odf1o2  19606  frlmlbs  21835  f1lindf  21860  2ndcdisj  23480  qtopf1  23840  clwlkclwwlklem2  30029  f1rnen  32646  erdszelem10  35185  pibt2  37400  dihfn  41251  dihcl  41253  dih1dimatlem  41312  dochocss  41349  onsucf1o  43262  cantnfub  43311  cantnfub2  43312  gricushgr  47824  grtrimap  47851