ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  f1f GIF version

Theorem f1f 5119
Description: A one-to-one mapping is a mapping. (Contributed by NM, 31-Dec-1996.)
Assertion
Ref Expression
f1f (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)

Proof of Theorem f1f
StepHypRef Expression
1 df-f1 4934 . 2 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
21simplbi 263 1 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  ccnv 4371  Fun wfun 4923  wf 4925  1-1wf1 4926
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114  df-f1 4934
This theorem is referenced by:  f1fn  5120  f1ss  5124  f1ssres  5126  f1of  5153  dff1o5  5162  fun11iun  5174  cocan1  5454  f1dmex  5770  f1o2ndf1  5876  brdomg  6259  f1dom2g  6266  f1domg  6268  dom3d  6284  f1imaen2g  6303  2dom  6315  xpdom2  6335  phplem4dom  6354
  Copyright terms: Public domain W3C validator