Theorem f1fn 6788

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

Syntax hints:   → wi 4   Fn wfn 6538  –1-1→wf1 6540

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 206  df-an 397  df-f 6547  df-f1 6548

This theorem is referenced by:  f1fun  6789  f1rel  6790  f1dm  6791  f1dmOLD  6792  f1ssr  6794  f1f1orn  6844  f1elima  7261  f1eqcocnv  7298  f1eqcocnvOLD  7299  domunsncan  9071  f1domfi2  9184  sbthfilem  9200  marypha2  9433  infdifsn  9651  acndom  10045  dfac12lem2  10138  ackbij1  10232  fin23lem32  10338  fin1a2lem5  10398  fin1a2lem6  10399  pwfseqlem1  10652  hashf1lem1  14414  hashf1lem1OLD  14415  hashf1  14417  odf1o2  19440  kerf1ghm  20281  frlmlbs  21351  f1lindf  21376  2ndcdisj  22959  qtopf1  23319  clwlkclwwlklem2  29250  f1rnen  31848  erdszelem10  34186  pibt2  36293  dihfn  40134  dihcl  40136  dih1dimatlem  40195  dochocss  40232  onsucf1o  42012  cantnfub  42061  cantnfub2  42062  isomushgr  46484