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

Definition df-nel 2315
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 2314 . 2 wff 𝐴𝐵
41, 2wcel 1409 . . 3 wff 𝐴𝐵
54wn 3 . 2 wff ¬ 𝐴𝐵
63, 5wb 102 1 wff (𝐴𝐵 ↔ ¬ 𝐴𝐵)
Colors of variables: wff set class
This definition is referenced by:  neli  2316  nelir  2317  neleq1  2318  neleq2  2319  nfnel  2321  nfneld  2322  ru  2786  sbcnel12g  2895  raldifb  3111  pwnss  3940  ruALT  4303  fiprc  6323  0mnnnnn0  8271  fvinim0ffz  9198  rennim  9829  bdnel  10361
  Copyright terms: Public domain W3C validator