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

Definition df-nel 2207
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 2205 . 2 wff 𝐴𝐵
41, 2wcel 1393 . . 3 wff 𝐴𝐵
54wn 3 . 2 wff ¬ 𝐴𝐵
63, 5wb 98 1 wff (𝐴𝐵 ↔ ¬ 𝐴𝐵)
Colors of variables: wff set class
This definition is referenced by:  neli  2299  nelir  2300  neleq1  2301  neleq2  2302  nfnel  2304  nfneld  2305  ru  2763  sbcnel12g  2867  raldifb  3083  pwnss  3912  ruALT  4275  fiprc  6292  0mnnnnn0  8212  fvinim0ffz  9094  rennim  9574  bdnel  9947
  Copyright terms: Public domain W3C validator