Type  Label  Description 
Statement 

Theorem  ssdifss 3201 
Preservation of a subclass relationship by class difference. (Contributed
by NM, 15Feb2007.)



Theorem  ddifnel 3202* 
Double complement under universal class. The hypothesis corresponds to
stability of membership in , which is weaker than decidability
(see dcstab 829). Actually, the conclusion is a
characterization of
stability of membership in a class (see ddifstab 3203) . Exercise 4.10(s)
of [Mendelson] p. 231, but with an
additional hypothesis. For a version
without a hypothesis, but which only states that is a subset of
, see ddifss 3309. (Contributed by Jim Kingdon,
21Jul2018.)



Theorem  ddifstab 3203* 
A class is equal to its double complement if and only if it is stable
(that is, membership in it is a stable property). (Contributed by BJ,
12Dec2021.)

STAB 

Theorem  ssconb 3204 
Contraposition law for subsets. (Contributed by NM, 22Mar1998.)



Theorem  sscon 3205 
Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22.
(Contributed by NM, 22Mar1998.)



Theorem  ssdif 3206 
Difference law for subsets. (Contributed by NM, 28May1998.)



Theorem  ssdifd 3207 
If is contained in
, then is contained in
.
Deduction form of ssdif 3206. (Contributed by David
Moews, 1May2017.)



Theorem  sscond 3208 
If is contained in
, then is contained in
.
Deduction form of sscon 3205. (Contributed by David
Moews, 1May2017.)



Theorem  ssdifssd 3209 
If is contained in
, then is also contained in
. Deduction
form of ssdifss 3201. (Contributed by David Moews,
1May2017.)



Theorem  ssdif2d 3210 
If is contained in
and is contained in , then
is
contained in .
Deduction form.
(Contributed by David Moews, 1May2017.)



Theorem  raldifb 3211 
Restricted universal quantification on a class difference in terms of an
implication. (Contributed by Alexander van der Vekens, 3Jan2018.)



2.1.13.2 The union of two classes


Theorem  elun 3212 
Expansion of membership in class union. Theorem 12 of [Suppes] p. 25.
(Contributed by NM, 7Aug1994.)



Theorem  uneqri 3213* 
Inference from membership to union. (Contributed by NM, 5Aug1993.)



Theorem  unidm 3214 
Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27.
(Contributed by NM, 5Aug1993.)



Theorem  uncom 3215 
Commutative law for union of classes. Exercise 6 of [TakeutiZaring]
p. 17. (Contributed by NM, 25Jun1998.) (Proof shortened by Andrew
Salmon, 26Jun2011.)



Theorem  equncom 3216 
If a class equals the union of two other classes, then it equals the union
of those two classes commuted. (Contributed by Alan Sare,
18Feb2012.)



Theorem  equncomi 3217 
Inference form of equncom 3216. (Contributed by Alan Sare,
18Feb2012.)



Theorem  uneq1 3218 
Equality theorem for union of two classes. (Contributed by NM,
5Aug1993.)



Theorem  uneq2 3219 
Equality theorem for the union of two classes. (Contributed by NM,
5Aug1993.)



Theorem  uneq12 3220 
Equality theorem for union of two classes. (Contributed by NM,
29Mar1998.)



Theorem  uneq1i 3221 
Inference adding union to the right in a class equality. (Contributed
by NM, 30Aug1993.)



Theorem  uneq2i 3222 
Inference adding union to the left in a class equality. (Contributed by
NM, 30Aug1993.)



Theorem  uneq12i 3223 
Equality inference for union of two classes. (Contributed by NM,
12Aug2004.) (Proof shortened by Eric Schmidt, 26Jan2007.)



Theorem  uneq1d 3224 
Deduction adding union to the right in a class equality. (Contributed
by NM, 29Mar1998.)



Theorem  uneq2d 3225 
Deduction adding union to the left in a class equality. (Contributed by
NM, 29Mar1998.)



Theorem  uneq12d 3226 
Equality deduction for union of two classes. (Contributed by NM,
29Sep2004.) (Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  nfun 3227 
Boundvariable hypothesis builder for the union of classes.
(Contributed by NM, 15Sep2003.) (Revised by Mario Carneiro,
14Oct2016.)



Theorem  unass 3228 
Associative law for union of classes. Exercise 8 of [TakeutiZaring]
p. 17. (Contributed by NM, 3May1994.) (Proof shortened by Andrew
Salmon, 26Jun2011.)



Theorem  un12 3229 
A rearrangement of union. (Contributed by NM, 12Aug2004.)



Theorem  un23 3230 
A rearrangement of union. (Contributed by NM, 12Aug2004.) (Proof
shortened by Andrew Salmon, 26Jun2011.)



Theorem  un4 3231 
A rearrangement of the union of 4 classes. (Contributed by NM,
12Aug2004.)



Theorem  unundi 3232 
Union distributes over itself. (Contributed by NM, 17Aug2004.)



Theorem  unundir 3233 
Union distributes over itself. (Contributed by NM, 17Aug2004.)



Theorem  ssun1 3234 
Subclass relationship for union of classes. Theorem 25 of [Suppes]
p. 27. (Contributed by NM, 5Aug1993.)



Theorem  ssun2 3235 
Subclass relationship for union of classes. (Contributed by NM,
30Aug1993.)



Theorem  ssun3 3236 
Subclass law for union of classes. (Contributed by NM, 5Aug1993.)



Theorem  ssun4 3237 
Subclass law for union of classes. (Contributed by NM, 14Aug1994.)



Theorem  elun1 3238 
Membership law for union of classes. (Contributed by NM, 5Aug1993.)



Theorem  elun2 3239 
Membership law for union of classes. (Contributed by NM, 30Aug1993.)



Theorem  unss1 3240 
Subclass law for union of classes. (Contributed by NM, 14Oct1999.)
(Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  ssequn1 3241 
A relationship between subclass and union. Theorem 26 of [Suppes]
p. 27. (Contributed by NM, 30Aug1993.) (Proof shortened by Andrew
Salmon, 26Jun2011.)



Theorem  unss2 3242 
Subclass law for union of classes. Exercise 7 of [TakeutiZaring] p. 18.
(Contributed by NM, 14Oct1999.)



Theorem  unss12 3243 
Subclass law for union of classes. (Contributed by NM, 2Jun2004.)



Theorem  ssequn2 3244 
A relationship between subclass and union. (Contributed by NM,
13Jun1994.)



Theorem  unss 3245 
The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27
and its converse. (Contributed by NM, 11Jun2004.)



Theorem  unssi 3246 
An inference showing the union of two subclasses is a subclass.
(Contributed by Raph Levien, 10Dec2002.)



Theorem  unssd 3247 
A deduction showing the union of two subclasses is a subclass.
(Contributed by Jonathan BenNaim, 3Jun2011.)



Theorem  unssad 3248 
If is contained
in , so is . Oneway
deduction form of unss 3245. Partial converse of unssd 3247. (Contributed
by David Moews, 1May2017.)



Theorem  unssbd 3249 
If is contained
in , so is . Oneway
deduction form of unss 3245. Partial converse of unssd 3247. (Contributed
by David Moews, 1May2017.)



Theorem  ssun 3250 
A condition that implies inclusion in the union of two classes.
(Contributed by NM, 23Nov2003.)



Theorem  rexun 3251 
Restricted existential quantification over union. (Contributed by Jeff
Madsen, 5Jan2011.)



Theorem  ralunb 3252 
Restricted quantification over a union. (Contributed by Scott Fenton,
12Apr2011.) (Proof shortened by Andrew Salmon, 29Jun2011.)



Theorem  ralun 3253 
Restricted quantification over union. (Contributed by Jeff Madsen,
2Sep2009.)



2.1.13.3 The intersection of two
classes


Theorem  elin 3254 
Expansion of membership in an intersection of two classes. Theorem 12
of [Suppes] p. 25. (Contributed by NM,
29Apr1994.)



Theorem  elini 3255 
Membership in an intersection of two classes. (Contributed by Glauco
Siliprandi, 17Aug2020.)



Theorem  elind 3256 
Deduce membership in an intersection of two classes. (Contributed by
Jonathan BenNaim, 3Jun2011.)



Theorem  elinel1 3257 
Membership in an intersection implies membership in the first set.
(Contributed by Glauco Siliprandi, 11Dec2019.)



Theorem  elinel2 3258 
Membership in an intersection implies membership in the second set.
(Contributed by Glauco Siliprandi, 11Dec2019.)



Theorem  elin2 3259 
Membership in a class defined as an intersection. (Contributed by
Stefan O'Rear, 29Mar2015.)



Theorem  elin1d 3260 
Elementhood in the first set of an intersection  deduction version.
(Contributed by Thierry Arnoux, 3May2020.)



Theorem  elin2d 3261 
Elementhood in the first set of an intersection  deduction version.
(Contributed by Thierry Arnoux, 3May2020.)



Theorem  elin3 3262 
Membership in a class defined as a ternary intersection. (Contributed
by Stefan O'Rear, 29Mar2015.)



Theorem  incom 3263 
Commutative law for intersection of classes. Exercise 7 of
[TakeutiZaring] p. 17.
(Contributed by NM, 5Aug1993.)



Theorem  ineqri 3264* 
Inference from membership to intersection. (Contributed by NM,
5Aug1993.)



Theorem  ineq1 3265 
Equality theorem for intersection of two classes. (Contributed by NM,
14Dec1993.)



Theorem  ineq2 3266 
Equality theorem for intersection of two classes. (Contributed by NM,
26Dec1993.)



Theorem  ineq12 3267 
Equality theorem for intersection of two classes. (Contributed by NM,
8May1994.)



Theorem  ineq1i 3268 
Equality inference for intersection of two classes. (Contributed by NM,
26Dec1993.)



Theorem  ineq2i 3269 
Equality inference for intersection of two classes. (Contributed by NM,
26Dec1993.)



Theorem  ineq12i 3270 
Equality inference for intersection of two classes. (Contributed by
NM, 24Jun2004.) (Proof shortened by Eric Schmidt, 26Jan2007.)



Theorem  ineq1d 3271 
Equality deduction for intersection of two classes. (Contributed by NM,
10Apr1994.)



Theorem  ineq2d 3272 
Equality deduction for intersection of two classes. (Contributed by NM,
10Apr1994.)



Theorem  ineq12d 3273 
Equality deduction for intersection of two classes. (Contributed by
NM, 24Jun2004.) (Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  ineqan12d 3274 
Equality deduction for intersection of two classes. (Contributed by
NM, 7Feb2007.)



Theorem  dfss1 3275 
A frequentlyused variant of subclass definition dfss 3079. (Contributed
by NM, 10Jan2015.)



Theorem  dfss5 3276 
Another definition of subclasshood. Similar to dfss 3079, dfss 3080, and
dfss1 3275. (Contributed by David Moews, 1May2017.)



Theorem  nfin 3277 
Boundvariable hypothesis builder for the intersection of classes.
(Contributed by NM, 15Sep2003.) (Revised by Mario Carneiro,
14Oct2016.)



Theorem  csbing 3278 
Distribute proper substitution through an intersection relation.
(Contributed by Alan Sare, 22Jul2012.)



Theorem  rabbi2dva 3279* 
Deduction from a wff to a restricted class abstraction. (Contributed by
NM, 14Jan2014.)



Theorem  inidm 3280 
Idempotent law for intersection of classes. Theorem 15 of [Suppes]
p. 26. (Contributed by NM, 5Aug1993.)



Theorem  inass 3281 
Associative law for intersection of classes. Exercise 9 of
[TakeutiZaring] p. 17.
(Contributed by NM, 3May1994.)



Theorem  in12 3282 
A rearrangement of intersection. (Contributed by NM, 21Apr2001.)



Theorem  in32 3283 
A rearrangement of intersection. (Contributed by NM, 21Apr2001.)
(Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  in13 3284 
A rearrangement of intersection. (Contributed by NM, 27Aug2012.)



Theorem  in31 3285 
A rearrangement of intersection. (Contributed by NM, 27Aug2012.)



Theorem  inrot 3286 
Rotate the intersection of 3 classes. (Contributed by NM,
27Aug2012.)



Theorem  in4 3287 
Rearrangement of intersection of 4 classes. (Contributed by NM,
21Apr2001.)



Theorem  inindi 3288 
Intersection distributes over itself. (Contributed by NM, 6May1994.)



Theorem  inindir 3289 
Intersection distributes over itself. (Contributed by NM,
17Aug2004.)



Theorem  sseqin2 3290 
A relationship between subclass and intersection. Similar to Exercise 9
of [TakeutiZaring] p. 18.
(Contributed by NM, 17May1994.)



Theorem  inss1 3291 
The intersection of two classes is a subset of one of them. Part of
Exercise 12 of [TakeutiZaring] p.
18. (Contributed by NM,
27Apr1994.)



Theorem  inss2 3292 
The intersection of two classes is a subset of one of them. Part of
Exercise 12 of [TakeutiZaring] p.
18. (Contributed by NM,
27Apr1994.)



Theorem  ssin 3293 
Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26.
(Contributed by NM, 15Jun2004.) (Proof shortened by Andrew Salmon,
26Jun2011.)



Theorem  ssini 3294 
An inference showing that a subclass of two classes is a subclass of
their intersection. (Contributed by NM, 24Nov2003.)



Theorem  ssind 3295 
A deduction showing that a subclass of two classes is a subclass of
their intersection. (Contributed by Jonathan BenNaim, 3Jun2011.)



Theorem  ssrin 3296 
Add right intersection to subclass relation. (Contributed by NM,
16Aug1994.) (Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  sslin 3297 
Add left intersection to subclass relation. (Contributed by NM,
19Oct1999.)



Theorem  ssrind 3298 
Add right intersection to subclass relation. (Contributed by Glauco
Siliprandi, 2Jan2022.)



Theorem  ss2in 3299 
Intersection of subclasses. (Contributed by NM, 5May2000.)



Theorem  ssinss1 3300 
Intersection preserves subclass relationship. (Contributed by NM,
14Sep1999.)

