![]() |
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 2454 | . 2 wff 𝐴 ∉ 𝐵 |
4 | 1, 2 | wcel 2159 | . . 3 wff 𝐴 ∈ 𝐵 |
5 | 4 | wn 3 | . 2 wff ¬ 𝐴 ∈ 𝐵 |
6 | 3, 5 | wb 105 | 1 wff (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) |
Colors of variables: wff set class |
This definition is referenced by: neli 2456 nelir 2457 neleq1 2458 neleq2 2459 nfnel 2461 nfneld 2462 elnelne1 2463 elnelne2 2464 nelcon3d 2465 elnelall 2466 ru 2975 sbcnel12g 3088 raldifb 3289 pwnss 4173 pwnex 4463 ruALT 4564 0nelrel 4686 fiprc 6832 0mnnnnn0 9225 fvinim0ffz 10258 rennim 11028 fsumsplitsnun 11444 modfsummodlemstep 11482 sqrt2irr0 12181 isnsgrp 12834 bdnel 14989 |
Copyright terms: Public domain | W3C validator |