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

Definition df-nel 2345
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 2344 . 2  wff  A  e/  B
41, 2wcel 1434 . . 3  wff  A  e.  B
54wn 3 . 2  wff  -.  A  e.  B
63, 5wb 103 1  wff  ( A  e/  B  <->  -.  A  e.  B )
Colors of variables: wff set class
This definition is referenced by:  neli  2346  nelir  2347  neleq1  2348  neleq2  2349  nfnel  2351  nfneld  2352  ru  2824  sbcnel12g  2933  raldifb  3123  pwnss  3954  ruALT  4323  fiprc  6383  0mnnnnn0  8464  fvinim0ffz  9404  rennim  10114  bdnel  10937
  Copyright terms: Public domain W3C validator