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

Definition df-nel 2456
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 2455 . 2  wff  A  e/  B
41, 2wcel 2160 . . 3  wff  A  e.  B
54wn 3 . 2  wff  -.  A  e.  B
63, 5wb 105 1  wff  ( A  e/  B  <->  -.  A  e.  B )
Colors of variables: wff set class
This definition is referenced by:  neli  2457  nelir  2458  neleq1  2459  neleq2  2460  nfnel  2462  nfneld  2463  elnelne1  2464  elnelne2  2465  nelcon3d  2466  elnelall  2467  ru  2976  sbcnel12g  3089  raldifb  3290  pwnss  4177  pwnex  4467  ruALT  4568  0nelrel  4690  fiprc  6841  0mnnnnn0  9238  fvinim0ffz  10271  rennim  11043  fsumsplitsnun  11459  modfsummodlemstep  11497  sqrt2irr0  12196  isnsgrp  12869  bdnel  15064
  Copyright terms: Public domain W3C validator