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

Definition df-nel 2404
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 class 𝐴
2 cB . . 3 class 𝐵
31, 2wnel 2403 . 2 wff 𝐴𝐵
41, 2wcel 1480 . . 3 wff 𝐴𝐵
54wn 3 . 2 wff ¬ 𝐴𝐵
63, 5wb 104 1 wff (𝐴𝐵 ↔ ¬ 𝐴𝐵)
Colors of variables: wff set class
This definition is referenced by:  neli  2405  nelir  2406  neleq1  2407  neleq2  2408  nfnel  2410  nfneld  2411  elnelne1  2412  elnelne2  2413  nelcon3d  2414  elnelall  2415  ru  2908  sbcnel12g  3019  raldifb  3216  pwnss  4083  pwnex  4370  ruALT  4466  0nelrel  4585  fiprc  6709  0mnnnnn0  9021  fvinim0ffz  10030  rennim  10786  fsumsplitsnun  11200  modfsummodlemstep  11238  sqrt2irr0  11853  bdnel  13111
  Copyright terms: Public domain W3C validator