![]() |
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 2205 | . 2 wff 𝐴 ∉ 𝐵 |
4 | 1, 2 | wcel 1393 | . . 3 wff 𝐴 ∈ 𝐵 |
5 | 4 | wn 3 | . 2 wff ¬ 𝐴 ∈ 𝐵 |
6 | 3, 5 | wb 98 | 1 wff (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) |
Colors of variables: wff set class |
This definition is referenced by: neli 2299 nelir 2300 neleq1 2301 neleq2 2302 nfnel 2304 nfneld 2305 ru 2763 sbcnel12g 2867 raldifb 3083 pwnss 3912 ruALT 4275 fiprc 6292 0mnnnnn0 8214 fvinim0ffz 9096 rennim 9600 bdnel 9974 |
Copyright terms: Public domain | W3C validator |