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  7970  rennim  9191  bdnel  9289
  Copyright terms: Public domain W3C validator