Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-ne | Unicode version |
Description: Define inequality. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
df-ne |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | 1, 2 | wne 2204 | . 2 |
4 | 1, 2 | wceq 1243 | . . 3 |
5 | 4 | wn 3 | . 2 |
6 | 3, 5 | wb 98 | 1 |
Colors of variables: wff set class |
This definition is referenced by: neii 2208 neir 2209 nner 2210 nnedc 2211 dcned 2212 neqned 2213 neirr 2215 dcne 2216 nonconne 2217 neeq1 2218 neeq2 2219 neneqd 2226 necon3abii 2241 necon3bii 2243 necon3abid 2244 necon3bid 2246 necon3ad 2247 necon3bd 2248 necon3d 2249 necon3ai 2254 necon3bi 2255 necon1aidc 2256 necon1bidc 2257 necon1idc 2258 necon2ai 2259 necon2ad 2262 necon2bd 2263 necon2d 2264 necon1abiidc 2265 necon1bbiidc 2266 necon1abiddc 2267 necon1bbiddc 2268 necon4aidc 2273 necon4idc 2274 necon4addc 2275 necon4bddc 2276 necon4ddc 2277 necon4abiddc 2278 necon4biddc 2280 necon1addc 2281 necon1bddc 2282 necon1ddc 2283 neanior 2292 ne3anior 2293 nemtbir 2294 nfne 2297 nfned 2298 sbcne12g 2868 dfpss2 3029 ifnefalse 3342 opthpr 3543 prneimg 3545 onsucelsucexmid 4255 nnsuc 4338 ftpg 5347 elni2 6412 indpi 6440 nngt1ne1 7948 zapne 8315 prime 8337 elnn1uz2 8544 xrnemnf 8699 xrnepnf 8700 flqeqceilz 9160 sqrt2irr 9878 algcvgblem 9888 bdne 9973 |
Copyright terms: Public domain | W3C validator |