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

Theorem f1f 5286
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 5086 . 2 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
21simplbi 270 1 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  ccnv 4498  Fun wfun 5075  wf 5077  1-1wf1 5078
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-f1 5086
This theorem is referenced by:  f1rn  5287  f1fn  5288  f1ss  5292  f1ssres  5295  f1of  5323  dff1o5  5332  cocan1  5642  f1o2ndf1  6079  brdomg  6596  f1dom2g  6604  f1domg  6606  dom3d  6622  f1imaen2g  6641  2dom  6653  xpdom2  6678  dom0  6685  phplem4dom  6709  isinfinf  6744  infm  6751  updjudhcoinlf  6917  updjudhcoinrg  6918  casef1  6927  djudom  6930  difinfsnlem  6936  difinfsn  6937  fihashf1rn  10428  ennnfonelemrn  11777  pwle2  12885
  Copyright terms: Public domain W3C validator