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

Definition df-nel 2204
Description: Define negated membership. (Contributed by NM, 7-Aug-1994.)
Assertion
Ref Expression
df-nel 
e/

Detailed syntax breakdown of Definition df-nel
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2wnel 2202 . 2  e/
41, 2wcel 1390 . . 3
54wn 3 . 2
63, 5wb 98 1  e/
Colors of variables: wff set class
This definition is referenced by:  neli  2293  nelir  2294  neleq1  2295  neleq2  2296  nfnel  2298  nfneld  2299  ru  2757  sbcnel12g  2861  raldifb  3077  pwnss  3903  ruALT  4229  fiprc  6228  0mnnnnn0  7990  rennim  9211  bdnel  9309
  Copyright terms: Public domain W3C validator