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

Definition df-nel 2315
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 2314 . 2  wff  A  e/  B
41, 2wcel 1409 . . 3  wff  A  e.  B
54wn 3 . 2  wff  -.  A  e.  B
63, 5wb 102 1  wff  ( A  e/  B  <->  -.  A  e.  B )
Colors of variables: wff set class
This definition is referenced by:  neli  2316  nelir  2317  neleq1  2318  neleq2  2319  nfnel  2321  nfneld  2322  ru  2785  sbcnel12g  2894  raldifb  3110  pwnss  3939  ruALT  4302  fiprc  6322  0mnnnnn0  8270  fvinim0ffz  9197  rennim  9828  bdnel  10340
  Copyright terms: Public domain W3C validator