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 2403 | . 2 wff 𝐴 ∉ 𝐵 |
4 | 1, 2 | wcel 1480 | . . 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 2405 nelir 2406 neleq1 2407 neleq2 2408 nfnel 2410 nfneld 2411 elnelne1 2412 elnelne2 2413 nelcon3d 2414 elnelall 2415 ru 2908 sbcnel12g 3019 raldifb 3216 pwnss 4083 pwnex 4370 ruALT 4466 0nelrel 4585 fiprc 6709 0mnnnnn0 9009 fvinim0ffz 10018 rennim 10774 fsumsplitsnun 11188 modfsummodlemstep 11226 sqrt2irr0 11842 bdnel 13052 |
Copyright terms: Public domain | W3C validator |