ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-nel Unicode version

Definition df-nel 2363
Description: Define negated membership. (Contributed by NM, 7-Aug-1994.)
Assertion
Ref Expression
df-nel  |-  ( A  e/  B  <->  -.  A  e.  B )

Detailed syntax breakdown of Definition df-nel
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2wnel 2362 . 2  wff  A  e/  B
41, 2wcel 1448 . . 3  wff  A  e.  B
54wn 3 . 2  wff  -.  A  e.  B
63, 5wb 104 1  wff  ( A  e/  B  <->  -.  A  e.  B )
Colors of variables: wff set class
This definition is referenced by:  neli  2364  nelir  2365  neleq1  2366  neleq2  2367  nfnel  2369  nfneld  2370  elnelne1  2371  elnelne2  2372  nelcon3d  2373  elnelall  2374  ru  2861  sbcnel12g  2970  raldifb  3163  pwnss  4023  pwnex  4308  ruALT  4404  0nelrel  4523  fiprc  6639  0mnnnnn0  8861  fvinim0ffz  9859  rennim  10614  fsumsplitsnun  11027  modfsummodlemstep  11065  bdnel  12633
  Copyright terms: Public domain W3C validator