Theorem f1fn 6777

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

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

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 6541  df-f1 6542

This theorem is used by:  f1fun  6778  f1funOLD  6779  f1relOLD  6781  f1dm  6782  f1ssr  6784  f1f1orn  6834  f1elima  7265  f1eqcocnv  7307  domunsncan  9089  f1domfi2  9190  sbthfilem  9206  fodomfir  9312  marypha2  9424  infdifsn  9651  acndom  10123  dfac12lem2  10216  ackbij1  10308  fin23lem32  10415  fin1a2lem5  10475  fin1a2lem6  10476  pwfseqlem1  10736  hashf1lem1  14593  hashf1  14595  kerf1ghm  19454  odf1o2  19780  frlmlbs  22096  f1lindf  22121  2ndcdisj  23768  qtopf1  24128  clwlkclwwlklem2  30584  f1rnen  33215  fineqvinfep  35776  vonf1wev  35870  erdszelem10  35944  pibt2  38320  dihfn  42305  dihcl  42307  dih1dimatlem  42366  dochocss  42403  onsucf1o  44258  cantnfub  44307  cantnfub2  44308  gricushgr  48984  grtrimap  49015