MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1fn Structured version   Visualization version   GIF version

Theorem f1fn 6671
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
StepHypRef Expression
1 f1f 6670 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
21ffnd 6601 1 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6428  1-1wf1 6430
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 6437  df-f1 6438
This theorem is referenced by:  f1fun  6672  f1rel  6673  f1dm  6674  f1dmOLD  6675  f1ssr  6677  f1f1orn  6727  f1elima  7136  f1eqcocnv  7173  f1eqcocnvOLD  7174  domunsncan  8859  f1domfi2  8968  sbthfilem  8984  marypha2  9198  infdifsn  9415  acndom  9807  dfac12lem2  9900  ackbij1  9994  fin23lem32  10100  fin1a2lem5  10160  fin1a2lem6  10161  pwfseqlem1  10414  hashf1lem1  14168  hashf1lem1OLD  14169  hashf1  14171  odf1o2  19178  kerf1ghm  19987  frlmlbs  21004  f1lindf  21029  2ndcdisj  22607  qtopf1  22967  clwlkclwwlklem2  28364  f1rnen  30964  erdszelem10  33162  pibt2  35588  dihfn  39282  dihcl  39284  dih1dimatlem  39343  dochocss  39380  isomushgr  45278
  Copyright terms: Public domain W3C validator