![]() |
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 2455 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | wcel 2160 |
. . 3
![]() ![]() ![]() ![]() |
5 | 4 | wn 3 |
. 2
![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: neli 2457 nelir 2458 neleq1 2459 neleq2 2460 nfnel 2462 nfneld 2463 elnelne1 2464 elnelne2 2465 nelcon3d 2466 elnelall 2467 ru 2976 sbcnel12g 3089 raldifb 3290 pwnss 4177 pwnex 4467 ruALT 4568 0nelrel 4690 fiprc 6841 0mnnnnn0 9238 fvinim0ffz 10271 rennim 11043 fsumsplitsnun 11459 modfsummodlemstep 11497 sqrt2irr0 12196 isnsgrp 12869 bdnel 15064 |
Copyright terms: Public domain | W3C validator |