![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-nel | GIF version |
Description: Define negated membership. (Contributed by NM, 7-Aug-1994.) |
Ref | Expression |
---|---|
df-nel | ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | wnel 2362 | . 2 wff 𝐴 ∉ 𝐵 |
4 | 1, 2 | wcel 1448 | . . 3 wff 𝐴 ∈ 𝐵 |
5 | 4 | wn 3 | . 2 wff ¬ 𝐴 ∈ 𝐵 |
6 | 3, 5 | wb 104 | 1 wff (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) |
Colors of variables: wff set class |
This definition is referenced by: neli 2364 nelir 2365 neleq1 2366 neleq2 2367 nfnel 2369 nfneld 2370 elnelne1 2371 elnelne2 2372 nelcon3d 2373 elnelall 2374 ru 2861 sbcnel12g 2970 raldifb 3163 pwnss 4023 pwnex 4308 ruALT 4404 0nelrel 4523 fiprc 6639 0mnnnnn0 8861 fvinim0ffz 9859 rennim 10614 fsumsplitsnun 11027 modfsummodlemstep 11065 bdnel 12633 |
Copyright terms: Public domain | W3C validator |