Theorem f1fn 6784

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 6538  –1-1→wf1 6540

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 6547  df-f1 6548

This theorem is used by:  f1fun  6785  f1funOLD  6786  f1relOLD  6788  f1dm  6789  f1ssr  6791  f1f1orn  6841  f1elima  7271  f1eqcocnv  7313  domunsncan  9103  f1domfi2  9204  sbthfilem  9220  fodomfir  9326  marypha2  9438  infdifsn  9665  acndom  10137  dfac12lem2  10230  ackbij1  10322  fin23lem32  10429  fin1a2lem5  10489  fin1a2lem6  10490  pwfseqlem1  10750  hashf1lem1  14607  hashf1  14609  kerf1ghm  19470  odf1o2  19796  frlmlbs  22112  f1lindf  22137  2ndcdisj  23784  qtopf1  24144  clwlkclwwlklem2  30600  f1rnen  33273  fineqvinfep  35853  vonf1wev  35959  erdszelem10  36055  pibt2  38449  dihfn  42434  dihcl  42436  dih1dimatlem  42495  dochocss  42532  onsucf1o  44383  cantnfub  44432  cantnfub2  44433  gricushgr  49123  grtrimap  49154