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

Definition df-nel 2455
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 2454 . 2 wff 𝐴𝐵
41, 2wcel 2159 . . 3 wff 𝐴𝐵
54wn 3 . 2 wff ¬ 𝐴𝐵
63, 5wb 105 1 wff (𝐴𝐵 ↔ ¬ 𝐴𝐵)
Colors of variables: wff set class
This definition is referenced by:  neli  2456  nelir  2457  neleq1  2458  neleq2  2459  nfnel  2461  nfneld  2462  elnelne1  2463  elnelne2  2464  nelcon3d  2465  elnelall  2466  ru  2975  sbcnel12g  3088  raldifb  3289  pwnss  4173  pwnex  4463  ruALT  4564  0nelrel  4686  fiprc  6832  0mnnnnn0  9225  fvinim0ffz  10258  rennim  11028  fsumsplitsnun  11444  modfsummodlemstep  11482  sqrt2irr0  12181  isnsgrp  12834  bdnel  14989
  Copyright terms: Public domain W3C validator