Type  Label  Description 
Statement 

2.1.4 Negated equality and
membership


Syntax  wne 2201 
Extend wff notation to include inequality.



Syntax  wnel 2202 
Extend wff notation to include negated membership.



Definition  dfne 2203 
Define inequality. (Contributed by NM, 5Aug1993.)



Definition  dfnel 2204 
Define negated membership. (Contributed by NM, 7Aug1994.)



2.1.4.1 Negated equality


Theorem  neii 2205 
Inference associated with dfne 2203. (Contributed by BJ, 7Jul2018.)



Theorem  neir 2206 
Inference associated with dfne 2203. (Contributed by BJ, 7Jul2018.)



Theorem  nner 2207 
Negation of inequality. (Contributed by Jim Kingdon, 23Dec2018.)



Theorem  nnedc 2208 
Negation of inequality where equality is decidable. (Contributed by Jim
Kingdon, 15May2018.)

DECID 

Theorem  dcned 2209 
Decidable equality implies decidable negated equality. (Contributed by
Jim Kingdon, 3May2020.)

DECID
DECID


Theorem  neirr 2210 
No class is unequal to itself. (Contributed by Stefan O'Rear,
1Jan2015.) (Proof rewritten by Jim Kingdon, 15May2018.)



Theorem  dcne 2211 
Decidable equality expressed in terms of . Basically the same as
dfdc 742. (Contributed by Jim Kingdon, 14Mar2020.)

DECID 

Theorem  nonconne 2212 
Law of noncontradiction with equality and inequality. (Contributed by NM,
3Feb2012.)



Theorem  neeq1 2213 
Equality theorem for inequality. (Contributed by NM, 19Nov1994.)



Theorem  neeq2 2214 
Equality theorem for inequality. (Contributed by NM, 19Nov1994.)



Theorem  neeq1i 2215 
Inference for inequality. (Contributed by NM, 29Apr2005.)



Theorem  neeq2i 2216 
Inference for inequality. (Contributed by NM, 29Apr2005.)



Theorem  neeq12i 2217 
Inference for inequality. (Contributed by NM, 24Jul2012.)



Theorem  neeq1d 2218 
Deduction for inequality. (Contributed by NM, 25Oct1999.)



Theorem  neeq2d 2219 
Deduction for inequality. (Contributed by NM, 25Oct1999.)



Theorem  neeq12d 2220 
Deduction for inequality. (Contributed by NM, 24Jul2012.)



Theorem  neneqd 2221 
Deduction eliminating inequality definition. (Contributed by Jonathan
BenNaim, 3Jun2011.)



Theorem  eqnetri 2222 
Substitution of equal classes into an inequality. (Contributed by NM,
4Jul2012.)



Theorem  eqnetrd 2223 
Substitution of equal classes into an inequality. (Contributed by NM,
4Jul2012.)



Theorem  eqnetrri 2224 
Substitution of equal classes into an inequality. (Contributed by NM,
4Jul2012.)



Theorem  eqnetrrd 2225 
Substitution of equal classes into an inequality. (Contributed by NM,
4Jul2012.)



Theorem  neeqtri 2226 
Substitution of equal classes into an inequality. (Contributed by NM,
4Jul2012.)



Theorem  neeqtrd 2227 
Substitution of equal classes into an inequality. (Contributed by NM,
4Jul2012.)



Theorem  neeqtrri 2228 
Substitution of equal classes into an inequality. (Contributed by NM,
4Jul2012.)



Theorem  neeqtrrd 2229 
Substitution of equal classes into an inequality. (Contributed by NM,
4Jul2012.)



Theorem  syl5eqner 2230 
B chained equality inference for inequality. (Contributed by NM,
6Jun2012.)



Theorem  3netr3d 2231 
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24Jul2012.)



Theorem  3netr4d 2232 
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24Jul2012.)



Theorem  3netr3g 2233 
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24Jul2012.)



Theorem  3netr4g 2234 
Substitution of equality into both sides of an inequality. (Contributed
by NM, 14Jun2012.)



Theorem  necon3abii 2235 
Deduction from equality to inequality. (Contributed by NM,
9Nov2007.)



Theorem  necon3bbii 2236 
Deduction from equality to inequality. (Contributed by NM,
13Apr2007.)



Theorem  necon3bii 2237 
Inference from equality to inequality. (Contributed by NM,
23Feb2005.)



Theorem  necon3abid 2238 
Deduction from equality to inequality. (Contributed by NM,
21Mar2007.)



Theorem  necon3bbid 2239 
Deduction from equality to inequality. (Contributed by NM,
2Jun2007.)



Theorem  necon3bid 2240 
Deduction from equality to inequality. (Contributed by NM,
23Feb2005.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  necon3ad 2241 
Contrapositive law deduction for inequality. (Contributed by NM,
2Apr2007.) (Proof rewritten by Jim Kingdon, 15May2018.)



Theorem  necon3bd 2242 
Contrapositive law deduction for inequality. (Contributed by NM,
2Apr2007.) (Proof rewritten by Jim Kingdon, 15May2018.)



Theorem  necon3d 2243 
Contrapositive law deduction for inequality. (Contributed by NM,
10Jun2006.)



Theorem  nesym 2244 
Characterization of inequality in terms of reversed equality (see
bicom 128). (Contributed by BJ, 7Jul2018.)



Theorem  nesymi 2245 
Inference associated with nesym 2244. (Contributed by BJ, 7Jul2018.)



Theorem  nesymir 2246 
Inference associated with nesym 2244. (Contributed by BJ, 7Jul2018.)



Theorem  necon3i 2247 
Contrapositive inference for inequality. (Contributed by NM,
9Aug2006.)



Theorem  necon3ai 2248 
Contrapositive inference for inequality. (Contributed by NM,
23May2007.) (Proof rewritten by Jim Kingdon, 15May2018.)



Theorem  necon3bi 2249 
Contrapositive inference for inequality. (Contributed by NM,
1Jun2007.) (Proof rewritten by Jim Kingdon, 15May2018.)



Theorem  necon1aidc 2250 
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
15May2018.)

DECID DECID 

Theorem  necon1bidc 2251 
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
15May2018.)

DECID DECID 

Theorem  necon1idc 2252 
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16May2018.)

DECID


Theorem  necon2ai 2253 
Contrapositive inference for inequality. (Contributed by NM,
16Jan2007.) (Proof rewritten by Jim Kingdon, 16May2018.)



Theorem  necon2bi 2254 
Contrapositive inference for inequality. (Contributed by NM,
1Apr2007.)



Theorem  necon2i 2255 
Contrapositive inference for inequality. (Contributed by NM,
18Mar2007.)



Theorem  necon2ad 2256 
Contrapositive inference for inequality. (Contributed by NM,
19Apr2007.) (Proof rewritten by Jim Kingdon, 16May2018.)



Theorem  necon2bd 2257 
Contrapositive inference for inequality. (Contributed by NM,
13Apr2007.)



Theorem  necon2d 2258 
Contrapositive inference for inequality. (Contributed by NM,
28Dec2008.)



Theorem  necon1abiidc 2259 
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16May2018.)

DECID DECID 

Theorem  necon1bbiidc 2260 
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16May2018.)

DECID DECID 

Theorem  necon1abiddc 2261 
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16May2018.)

DECID DECID 

Theorem  necon1bbiddc 2262 
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16May2018.)

DECID DECID


Theorem  necon2abiidc 2263 
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16May2018.)

DECID DECID 

Theorem  necon2bbii 2264 
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16May2018.)

DECID DECID 

Theorem  necon2abiddc 2265 
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16May2018.)

DECID DECID 

Theorem  necon2bbiddc 2266 
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16May2018.)

DECID DECID 

Theorem  necon4aidc 2267 
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16May2018.)

DECID DECID 

Theorem  necon4idc 2268 
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16May2018.)

DECID DECID


Theorem  necon4addc 2269 
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17May2018.)

DECID DECID 

Theorem  necon4bddc 2270 
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17May2018.)

DECID DECID 

Theorem  necon4ddc 2271 
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17May2018.)

DECID DECID 

Theorem  necon4abiddc 2272 
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 18May2018.)

DECID DECID DECID DECID 

Theorem  necon4bbiddc 2273 
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19May2018.)

DECID DECID DECID DECID 

Theorem  necon4biddc 2274 
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19May2018.)

DECID DECID DECID DECID 

Theorem  necon1addc 2275 
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
19May2018.)

DECID DECID 

Theorem  necon1bddc 2276 
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
19May2018.)

DECID DECID 

Theorem  necon1ddc 2277 
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19May2018.)

DECID DECID 

Theorem  neneqad 2278 
If it is not the case that two classes are equal, they are unequal.
Converse of neneqd 2221. Oneway deduction form of dfne 2203.
(Contributed by David Moews, 28Feb2017.)



Theorem  nebidc 2279 
Contraposition law for inequality. (Contributed by Jim Kingdon,
19May2018.)

DECID DECID


Theorem  pm13.18 2280 
Theorem *13.18 in [WhiteheadRussell]
p. 178. (Contributed by Andrew
Salmon, 3Jun2011.)



Theorem  pm13.181 2281 
Theorem *13.181 in [WhiteheadRussell]
p. 178. (Contributed by Andrew
Salmon, 3Jun2011.)



Theorem  pm2.21ddne 2282 
A contradiction implies anything. Equality/inequality deduction form.
(Contributed by David Moews, 28Feb2017.)



Theorem  necom 2283 
Commutation of inequality. (Contributed by NM, 14May1999.)



Theorem  necomi 2284 
Inference from commutative law for inequality. (Contributed by NM,
17Oct2012.)



Theorem  necomd 2285 
Deduction from commutative law for inequality. (Contributed by NM,
12Feb2008.)



Theorem  neanior 2286 
A De Morgan's law for inequality. (Contributed by NM, 18May2007.)



Theorem  ne3anior 2287 
A De Morgan's law for inequality. (Contributed by NM, 30Sep2013.)
(Proof rewritten by Jim Kingdon, 19May2018.)



Theorem  nemtbir 2288 
An inference from an inequality, related to modus tollens. (Contributed
by NM, 13Apr2007.)



Theorem  nelne1 2289 
Two classes are different if they don't contain the same element.
(Contributed by NM, 3Feb2012.)



Theorem  nelne2 2290 
Two classes are different if they don't belong to the same class.
(Contributed by NM, 25Jun2012.)



Theorem  nfne 2291 
Boundvariable hypothesis builder for inequality. (Contributed by NM,
10Nov2007.) (Revised by Mario Carneiro, 7Oct2016.)



Theorem  nfned 2292 
Boundvariable hypothesis builder for inequality. (Contributed by NM,
10Nov2007.) (Revised by Mario Carneiro, 7Oct2016.)



2.1.4.2 Negated membership


Theorem  neli 2293 
Inference associated with dfnel 2204. (Contributed by BJ,
7Jul2018.)



Theorem  nelir 2294 
Inference associated with dfnel 2204. (Contributed by BJ,
7Jul2018.)



Theorem  neleq1 2295 
Equality theorem for negated membership. (Contributed by NM,
20Nov1994.)



Theorem  neleq2 2296 
Equality theorem for negated membership. (Contributed by NM,
20Nov1994.)



Theorem  neleq12d 2297 
Equality theorem for negated membership. (Contributed by FL,
10Aug2016.)



Theorem  nfnel 2298 
Boundvariable hypothesis builder for negated membership. (Contributed
by David Abernethy, 26Jun2011.) (Revised by Mario Carneiro,
7Oct2016.)



Theorem  nfneld 2299 
Boundvariable hypothesis builder for negated membership. (Contributed
by David Abernethy, 26Jun2011.) (Revised by Mario Carneiro,
7Oct2016.)



2.1.5 Restricted quantification


Syntax  wral 2300 
Extend wff notation to include restricted universal quantification.

