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

Definition df-nel 2347
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 2346 . 2 wff 𝐴𝐵
41, 2wcel 1436 . . 3 wff 𝐴𝐵
54wn 3 . 2 wff ¬ 𝐴𝐵
63, 5wb 103 1 wff (𝐴𝐵 ↔ ¬ 𝐴𝐵)
Colors of variables: wff set class
This definition is referenced by:  neli  2348  nelir  2349  neleq1  2350  neleq2  2351  nfnel  2353  nfneld  2354  ru  2828  sbcnel12g  2937  raldifb  3129  pwnss  3971  ruALT  4342  fiprc  6486  0mnnnnn0  8641  fvinim0ffz  9583  rennim  10334  fsumsplitsnun  10700  bdnel  11214
  Copyright terms: Public domain W3C validator