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

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

Detailed syntax breakdown of Definition df-nel
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2wnel 2517 . 2 wff A B
41, 2wcel 1710 . . 3 wff A B
54wn 3 . 2 wff ¬ A B
63, 5wb 176 1 wff (A B ↔ ¬ A B)
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