NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-nel Unicode version

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

Detailed syntax breakdown of Definition df-nel
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2wnel 2517 . 2
41, 2wcel 1710 . . 3
54wn 3 . 2
63, 5wb 176 1
Colors of variables: wff setvar class
This definition is referenced by:  neleq1  2607  neleq2  2608  nfnel  2611  nfneld  2613  ru  3045  sbcnel12g  3153  epprc  5827
  Copyright terms: Public domain W3C validator