Type  Label  Description 
Statement 

Theorem  cleqf 2201 
Establish equality between classes, using boundvariable hypotheses
instead of distinct variable conditions. See also cleqh 2137.
(Contributed by NM, 5Aug1993.) (Revised by Mario Carneiro,
7Oct2016.)



Theorem  abid2f 2202 
A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35.
(Contributed by NM, 5Sep2011.) (Revised by Mario Carneiro,
7Oct2016.)



Theorem  sbabel 2203* 
Theorem to move a substitution in and out of a class abstraction.
(Contributed by NM, 27Sep2003.) (Revised by Mario Carneiro,
7Oct2016.)



2.1.4 Negated equality and
membership


Syntax  wne 2204 
Extend wff notation to include inequality.



Syntax  wnel 2205 
Extend wff notation to include negated membership.



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



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



2.1.4.1 Negated equality


Theorem  neii 2208 
Inference associated with dfne 2206. (Contributed by BJ, 7Jul2018.)



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



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



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

DECID 

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

DECID
DECID


Theorem  neqned 2213 
If it is not the case that two classes are equal, they are unequal.
Converse of neneqd 2226. Oneway deduction form of dfne 2206.
(Contributed by David Moews, 28Feb2017.) Allow a shortening of
necon3bi 2255. (Revised by Wolf Lammen, 22Nov2019.)



Theorem  neqne 2214 
From non equality to inequality. (Contributed by Glauco Siliprandi,
11Dec2019.)



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



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

DECID 

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



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



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



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



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



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



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



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



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



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



Theorem  neneq 2227 
From inequality to non equality. (Contributed by Glauco Siliprandi,
11Dec2019.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  nesymi 2251 
Inference associated with nesym 2250. (Contributed by BJ, 7Jul2018.)



Theorem  nesymir 2252 
Inference associated with nesym 2250. (Contributed by BJ, 7Jul2018.)



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



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



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



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

DECID DECID 

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

DECID DECID


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

DECID


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



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



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



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



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



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



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

DECID DECID 

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

DECID DECID


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

DECID
DECID 

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

DECID
DECID


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

DECID DECID


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

DECID DECID 

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

DECID
DECID


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

DECID
DECID


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

DECID DECID 

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

DECID DECID


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

DECID
DECID 

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

DECID DECID 

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

DECID
DECID


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

DECID
DECID DECID
DECID 

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

DECID DECID
DECID DECID


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

DECID
DECID DECID
DECID 

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

DECID DECID 

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

DECID
DECID


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

DECID
DECID


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



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

DECID DECID 

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



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



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



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



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



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



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



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



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



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



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



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



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



2.1.4.2 Negated membership


Theorem  neli 2299 
Inference associated with dfnel 2207. (Contributed by BJ,
7Jul2018.)



Theorem  nelir 2300 
Inference associated with dfnel 2207. (Contributed by BJ,
7Jul2018.)

