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

Definition df-nel 2404
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 2403 . 2  wff  A  e/  B
41, 2wcel 1480 . . 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  2405  nelir  2406  neleq1  2407  neleq2  2408  nfnel  2410  nfneld  2411  elnelne1  2412  elnelne2  2413  nelcon3d  2414  elnelall  2415  ru  2908  sbcnel12g  3019  raldifb  3216  pwnss  4083  pwnex  4370  ruALT  4466  0nelrel  4585  fiprc  6709  0mnnnnn0  9023  fvinim0ffz  10032  rennim  10788  fsumsplitsnun  11202  modfsummodlemstep  11240  sqrt2irr0  11855  bdnel  13159
  Copyright terms: Public domain W3C validator