Theorem f1fn 6000

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 5999	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		ffn 5944	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 5785  ⟶wf 5786  –1-1→wf1 5787

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 196  df-an 385  df-f 5794  df-f1 5795

This theorem is referenced by:  f1fun  6001  f1rel  6002  f1dm  6003  f1ssr  6005  f1f1orn  6046  f1elima  6399  f1eqcocnv  6434  domunsncan  7923  marypha2  8206  infdifsn  8415  acndom  8735  dfac12lem2  8827  ackbij1  8921  fin23lem32  9027  fin1a2lem5  9087  fin1a2lem6  9088  pwfseqlem1  9337  hashf1lem1  13051  hashf1  13053  odf1o2  17760  kerf1hrm  18515  frlmlbs  19903  f1lindf  19928  2ndcdisj  21017  qtopf1  21377  usgraedgrn  25704  usgfidegfi  26231  erdszelem10  30230  dihfn  35369  dihcl  35371  dih1dimatlem  35430  dochocss  35467  clwlkclwwlklem2  41201