Type  Label  Description 
Statement 

Theorem  nfeq 2201 
Hypothesis builder for equality. (Contributed by Mario Carneiro,
11Aug2016.)



Theorem  nfel 2202 
Hypothesis builder for elementhood. (Contributed by Mario Carneiro,
11Aug2016.)



Theorem  nfeq1 2203* 
Hypothesis builder for equality, special case. (Contributed by Mario
Carneiro, 10Oct2016.)



Theorem  nfel1 2204* 
Hypothesis builder for elementhood, special case. (Contributed by Mario
Carneiro, 10Oct2016.)



Theorem  nfeq2 2205* 
Hypothesis builder for equality, special case. (Contributed by Mario
Carneiro, 10Oct2016.)



Theorem  nfel2 2206* 
Hypothesis builder for elementhood, special case. (Contributed by Mario
Carneiro, 10Oct2016.)



Theorem  nfcrd 2207* 
Consequence of the notfree predicate. (Contributed by Mario Carneiro,
11Aug2016.)



Theorem  nfeqd 2208 
Hypothesis builder for equality. (Contributed by Mario Carneiro,
7Oct2016.)



Theorem  nfeld 2209 
Hypothesis builder for elementhood. (Contributed by Mario Carneiro,
7Oct2016.)



Theorem  drnfc1 2210 
Formulabuilding lemma for use with the Distinctor Reduction Theorem.
(Contributed by Mario Carneiro, 8Oct2016.)



Theorem  drnfc2 2211 
Formulabuilding lemma for use with the Distinctor Reduction Theorem.
(Contributed by Mario Carneiro, 8Oct2016.)



Theorem  nfabd 2212 
Boundvariable hypothesis builder for a class abstraction. (Contributed
by Mario Carneiro, 8Oct2016.)



Theorem  dvelimdc 2213 
Deduction form of dvelimc 2214. (Contributed by Mario Carneiro,
8Oct2016.)



Theorem  dvelimc 2214 
Version of dvelim 1909 for classes. (Contributed by Mario Carneiro,
8Oct2016.)



Theorem  nfcvf 2215 
If and are distinct, then is not free in .
(Contributed by Mario Carneiro, 8Oct2016.)



Theorem  nfcvf2 2216 
If and are distinct, then is not free in .
(Contributed by Mario Carneiro, 5Dec2016.)



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



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



Theorem  sbabel 2219* 
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


2.1.4.1 Negated equality


Syntax  wne 2220 
Extend wff notation to include inequality.



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



Theorem  neii 2222 
Inference associated with dfne 2221. (Contributed by BJ, 7Jul2018.)



Theorem  neir 2223 
Inference associated with dfne 2221. (Contributed by BJ, 7Jul2018.)



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



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

DECID 

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

DECID
DECID


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



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



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



Theorem  eqneqall 2230 
A contradiction concerning equality implies anything. (Contributed by
Alexander van der Vekens, 25Jan2018.)



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

DECID 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  nesymi 2266 
Inference associated with nesym 2265. (Contributed by BJ, 7Jul2018.)



Theorem  nesymir 2267 
Inference associated with nesym 2265. (Contributed by BJ, 7Jul2018.)



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



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



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



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

DECID DECID 

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

DECID DECID


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

DECID


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



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



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



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



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



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



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

DECID DECID 

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

DECID DECID


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

DECID
DECID 

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

DECID
DECID


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

DECID DECID


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

DECID DECID 

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

DECID
DECID


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

DECID
DECID


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

DECID DECID 

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

DECID DECID


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

DECID
DECID 

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

DECID DECID 

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

DECID
DECID


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

DECID
DECID DECID
DECID 

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

DECID DECID
DECID DECID


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

DECID
DECID DECID
DECID 

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

DECID DECID 

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

DECID
DECID


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

DECID
DECID


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



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

DECID DECID 