Theorem f1fn 6794

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

Syntax hints:   → wi 4   Fn wfn 6543  –1-1→wf1 6545

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 396  df-f 6552  df-f1 6553

This theorem is referenced by:  f1fun  6795  f1rel  6796  f1dm  6797  f1dmOLD  6798  f1ssr  6800  f1f1orn  6850  f1elima  7273  f1eqcocnv  7310  f1eqcocnvOLD  7311  domunsncan  9097  f1domfi2  9210  sbthfilem  9226  marypha2  9463  infdifsn  9681  acndom  10075  dfac12lem2  10168  ackbij1  10262  fin23lem32  10368  fin1a2lem5  10428  fin1a2lem6  10429  pwfseqlem1  10682  hashf1lem1  14448  hashf1lem1OLD  14449  hashf1  14451  kerf1ghm  19201  odf1o2  19528  frlmlbs  21731  f1lindf  21756  2ndcdisj  23373  qtopf1  23733  clwlkclwwlklem2  29823  f1rnen  32427  erdszelem10  34810  pibt2  36896  dihfn  40741  dihcl  40743  dih1dimatlem  40802  dochocss  40839  onsucf1o  42701  cantnfub  42750  cantnfub2  42751  gricushgr  47183