![]() |
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 2344 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | wcel 1434 |
. . 3
![]() ![]() ![]() ![]() |
5 | 4 | wn 3 |
. 2
![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | wb 103 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: neli 2346 nelir 2347 neleq1 2348 neleq2 2349 nfnel 2351 nfneld 2352 ru 2824 sbcnel12g 2933 raldifb 3123 pwnss 3954 ruALT 4323 fiprc 6383 0mnnnnn0 8464 fvinim0ffz 9404 rennim 10114 bdnel 10937 |
Copyright terms: Public domain | W3C validator |