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

Theorem f1f 5162
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 4972 . 2 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
21simplbi 268 1 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  ccnv 4398  Fun wfun 4961  wf 4963  1-1wf1 4964
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-f1 4972
This theorem is referenced by:  f1rn  5163  f1fn  5164  f1ss  5168  f1ssres  5171  f1of  5199  dff1o5  5208  cocan1  5504  f1o2ndf1  5926  brdomg  6393  f1dom2g  6401  f1domg  6403  dom3d  6419  f1imaen2g  6438  2dom  6450  xpdom2  6475  dom0  6482  phplem4dom  6506  isinfinf  6541  infm  6545  updjudhcoinlf  6676  updjudhcoinrg  6677  casef1  6686  djudom  6692  fihashf1rn  10030
  Copyright terms: Public domain W3C validator