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

Theorem f1f 5421
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 5221 . 2 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
21simplbi 274 1 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  ccnv 4625  Fun wfun 5210  wf 5212  1-1wf1 5213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117  df-f1 5221
This theorem is referenced by:  f1rn  5422  f1fn  5423  f1ss  5427  f1ssres  5430  f1of  5461  dff1o5  5470  fsnd  5504  cocan1  5787  f1o2ndf1  6228  brdomg  6747  f1dom2g  6755  f1domg  6757  dom3d  6773  f1imaen2g  6792  2dom  6804  xpdom2  6830  dom0  6837  phplem4dom  6861  isinfinf  6896  infm  6903  updjudhcoinlf  7078  updjudhcoinrg  7079  casef1  7088  djudom  7091  difinfsnlem  7097  difinfsn  7098  fihashf1rn  10767  ennnfonelemrn  12419  reeff1o  14164  pwle2  14718
  Copyright terms: Public domain W3C validator