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

Theorem f1fn 6263
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 6262 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
2 ffn 6206 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 1 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6044  wf 6045  1-1wf1 6046
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 197  df-an 385  df-f 6053  df-f1 6054
This theorem is referenced by:  f1fun  6264  f1rel  6265  f1dm  6266  f1ssr  6268  f1f1orn  6309  f1elima  6683  f1eqcocnv  6719  domunsncan  8225  marypha2  8510  infdifsn  8727  acndom  9064  dfac12lem2  9158  ackbij1  9252  fin23lem32  9358  fin1a2lem5  9418  fin1a2lem6  9419  pwfseqlem1  9672  hashf1lem1  13431  hashf1  13433  odf1o2  18188  kerf1hrm  18945  frlmlbs  20338  f1lindf  20363  2ndcdisj  21461  qtopf1  21821  clwlkclwwlklem2  27123  erdszelem10  31489  dihfn  37059  dihcl  37061  dih1dimatlem  37120  dochocss  37157
  Copyright terms: Public domain W3C validator