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

Definition df-nel 2381
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 2380 . 2 wff 𝐴𝐵
41, 2wcel 1465 . . 3 wff 𝐴𝐵
54wn 3 . 2 wff ¬ 𝐴𝐵
63, 5wb 104 1 wff (𝐴𝐵 ↔ ¬ 𝐴𝐵)
Colors of variables: wff set class
This definition is referenced by:  neli  2382  nelir  2383  neleq1  2384  neleq2  2385  nfnel  2387  nfneld  2388  elnelne1  2389  elnelne2  2390  nelcon3d  2391  elnelall  2392  ru  2881  sbcnel12g  2990  raldifb  3186  pwnss  4053  pwnex  4340  ruALT  4436  0nelrel  4555  fiprc  6677  0mnnnnn0  8967  fvinim0ffz  9973  rennim  10729  fsumsplitsnun  11143  modfsummodlemstep  11181  bdnel  12948
  Copyright terms: Public domain W3C validator