Type  Label  Description 
Statement 

Theorem  abbi 2201 
Equivalent wff's correspond to equal class abstractions. (Contributed
by NM, 25Nov2013.) (Revised by Mario Carneiro, 11Aug2016.)



Theorem  abbi2i 2202* 
Equality of a class variable and a class abstraction (inference form).
(Contributed by NM, 5Aug1993.)



Theorem  abbii 2203 
Equivalent wff's yield equal class abstractions (inference form).
(Contributed by NM, 5Aug1993.)



Theorem  abbid 2204 
Equivalent wff's yield equal class abstractions (deduction form).
(Contributed by NM, 5Aug1993.) (Revised by Mario Carneiro,
7Oct2016.)



Theorem  abbidv 2205* 
Equivalent wff's yield equal class abstractions (deduction form).
(Contributed by NM, 10Aug1993.)



Theorem  abbi2dv 2206* 
Deduction from a wff to a class abstraction. (Contributed by NM,
9Jul1994.)



Theorem  abbi1dv 2207* 
Deduction from a wff to a class abstraction. (Contributed by NM,
9Jul1994.)



Theorem  abid2 2208* 
A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35.
(Contributed by NM, 26Dec1993.)



Theorem  sb8ab 2209 
Substitution of variable in class abstraction. (Contributed by Jim
Kingdon, 27Sep2018.)



Theorem  cbvab 2210 
Rule used to change bound variables, using implicit substitution.
(Contributed by Andrew Salmon, 11Jul2011.)



Theorem  cbvabv 2211* 
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 26May1999.)



Theorem  clelab 2212* 
Membership of a class variable in a class abstraction. (Contributed by
NM, 23Dec1993.)



Theorem  clabel 2213* 
Membership of a class abstraction in another class. (Contributed by NM,
17Jan2006.)



Theorem  sbab 2214* 
The righthand side of the second equality is a way of representing
proper substitution of for into a
class variable.
(Contributed by NM, 14Sep2003.)



2.1.3 Class form notfree predicate


Syntax  wnfc 2215 
Extend wff definition to include the notfree predicate for classes.



Theorem  nfcjust 2216* 
Justification theorem for dfnfc 2217. (Contributed by Mario Carneiro,
13Oct2016.)



Definition  dfnfc 2217* 
Define the notfree predicate for classes. This is read " is not
free in ".
Notfree means that the value of cannot affect
the value of ,
e.g., any occurrence of in is
effectively bound by a quantifier or something that expands to one (such
as "there exists at most one"). It is defined in terms of the
notfree
predicate dfnf 1395 for wffs; see that definition for more
information.
(Contributed by Mario Carneiro, 11Aug2016.)



Theorem  nfci 2218* 
Deduce that a class
does not have free in
it.
(Contributed by Mario Carneiro, 11Aug2016.)



Theorem  nfcii 2219* 
Deduce that a class
does not have free in
it.
(Contributed by Mario Carneiro, 11Aug2016.)



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



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



Theorem  nfcri 2222* 
Consequence of the notfree predicate. (Note that unlike nfcr 2220,
this
does not require
and to be disjoint.)
(Contributed by Mario
Carneiro, 11Aug2016.)



Theorem  nfcd 2223* 
Deduce that a class
does not have free in
it. (Contributed
by Mario Carneiro, 11Aug2016.)



Theorem  nfceqi 2224 
Equality theorem for class notfree. (Contributed by Mario Carneiro,
11Aug2016.)



Theorem  nfcxfr 2225 
A utility lemma to transfer a boundvariable hypothesis builder into a
definition. (Contributed by Mario Carneiro, 11Aug2016.)



Theorem  nfcxfrd 2226 
A utility lemma to transfer a boundvariable hypothesis builder into a
definition. (Contributed by Mario Carneiro, 11Aug2016.)



Theorem  nfceqdf 2227 
An equality theorem for effectively not free. (Contributed by Mario
Carneiro, 14Oct2016.)



Theorem  nfcv 2228* 
If is disjoint from
, then is not free in .
(Contributed by Mario Carneiro, 11Aug2016.)



Theorem  nfcvd 2229* 
If is disjoint from
, then is not free in .
(Contributed by Mario Carneiro, 7Oct2016.)



Theorem  nfab1 2230 
Boundvariable hypothesis builder for a class abstraction. (Contributed
by Mario Carneiro, 11Aug2016.)



Theorem  nfnfc1 2231 
is bound in . (Contributed by Mario Carneiro,
11Aug2016.)



Theorem  clelsb3f 2232 
Substitution applied to an atomic wff (class version of elsb3 1900).
(Contributed by Rodolfo Medina, 28Apr2010.) (Proof shortened by
Andrew Salmon, 14Jun2011.) (Revised by Thierry Arnoux,
13Mar2017.)



Theorem  nfab 2233 
Boundvariable hypothesis builder for a class abstraction. (Contributed
by Mario Carneiro, 11Aug2016.)



Theorem  nfaba1 2234 
Boundvariable hypothesis builder for a class abstraction. (Contributed
by Mario Carneiro, 14Oct2016.)



Theorem  nfnfc 2235 
Hypothesis builder for . (Contributed by Mario
Carneiro,
11Aug2016.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  sbabel 2254* 
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 2255 
Extend wff notation to include inequality.



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



Theorem  neii 2257 
Inference associated with dfne 2256. (Contributed by BJ, 7Jul2018.)



Theorem  neir 2258 
Inference associated with dfne 2256. (Contributed by BJ, 7Jul2018.)



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



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

DECID 

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

DECID
DECID


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



Theorem  neqne 2263 
From nonequality to inequality. (Contributed by Glauco Siliprandi,
11Dec2019.)



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



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



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

DECID 

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



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



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



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



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



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



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



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



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



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



Theorem  neneq 2277 
From inequality to nonequality. (Contributed by Glauco Siliprandi,
11Dec2019.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

