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

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

Detailed syntax breakdown of Definition df-nel
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2wnel 2202 . 2 wff AB
41, 2wcel 1390 . . 3 wff A B
54wn 3 . 2 wff ¬ A B
63, 5wb 98 1 wff (AB ↔ ¬ A B)
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  7950  bdnel  9243
  Copyright terms: Public domain W3C validator