Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-nel | Unicode version |
Description: Define negated membership. (Contributed by NM, 7-Aug-1994.) |
Ref | Expression |
---|---|
df-nel |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | 1, 2 | wnel 2380 | . 2 |
4 | 1, 2 | wcel 1465 | . . 3 |
5 | 4 | wn 3 | . 2 |
6 | 3, 5 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: neli 2382 nelir 2383 neleq1 2384 neleq2 2385 nfnel 2387 nfneld 2388 elnelne1 2389 elnelne2 2390 nelcon3d 2391 elnelall 2392 ru 2881 sbcnel12g 2990 raldifb 3186 pwnss 4053 pwnex 4340 ruALT 4436 0nelrel 4555 fiprc 6677 0mnnnnn0 8967 fvinim0ffz 9973 rennim 10729 fsumsplitsnun 11143 modfsummodlemstep 11181 bdnel 12948 |
Copyright terms: Public domain | W3C validator |