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 6495  –1-1→wf1 6497

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

This theorem is referenced by:  f1fun  6740  f1rel  6741  f1dm  6742  f1ssr  6744  f1f1orn  6793  f1elima  7219  f1eqcocnv  7257  domunsncan  9017  f1domfi2  9118  sbthfilem  9134  fodomfir  9240  marypha2  9354  infdifsn  9578  acndom  9973  dfac12lem2  10067  ackbij1  10159  fin23lem32  10266  fin1a2lem5  10326  fin1a2lem6  10327  pwfseqlem1  10581  hashf1lem1  14390  hashf1  14392  kerf1ghm  19188  odf1o2  19514  frlmlbs  21764  f1lindf  21789  2ndcdisj  23412  qtopf1  23772  clwlkclwwlklem2  30087  f1rnen  32718  fineqvinfep  35303  erdszelem10  35416  pibt2  37672  dihfn  41644  dihcl  41646  dih1dimatlem  41705  dochocss  41742  onsucf1o  43629  cantnfub  43678  cantnfub2  43679  gricushgr  48277  grtrimap  48308