Theorem f1fn 6818

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

Syntax hints:   → wi 4   Fn wfn 6568  –1-1→wf1 6570

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 6577  df-f1 6578

This theorem is referenced by:  f1fun  6819  f1rel  6820  f1dm  6821  f1ssr  6823  f1f1orn  6873  f1elima  7300  f1eqcocnv  7337  domunsncan  9138  f1domfi2  9248  sbthfilem  9264  fodomfir  9396  marypha2  9508  infdifsn  9726  acndom  10120  dfac12lem2  10214  ackbij1  10306  fin23lem32  10413  fin1a2lem5  10473  fin1a2lem6  10474  pwfseqlem1  10727  hashf1lem1  14504  hashf1  14506  kerf1ghm  19287  odf1o2  19615  frlmlbs  21840  f1lindf  21865  2ndcdisj  23485  qtopf1  23845  clwlkclwwlklem2  30032  f1rnen  32648  erdszelem10  35168  pibt2  37383  dihfn  41225  dihcl  41227  dih1dimatlem  41286  dochocss  41323  onsucf1o  43234  cantnfub  43283  cantnfub2  43284  gricushgr  47770  grtrimap  47797