Type  Label  Description 
Statement 

Theorem  ss2abdv 3201* 
Deduction of abstraction subclass from implication. (Contributed by NM,
29Jul2011.)



Theorem  abssdv 3202* 
Deduction of abstraction subclass from implication. (Contributed by NM,
20Jan2006.)



Theorem  abssi 3203* 
Inference of abstraction subclass from implication. (Contributed by NM,
20Jan2006.)



Theorem  ss2rab 3204 
Restricted abstraction classes in a subclass relationship. (Contributed
by NM, 30May1999.)



Theorem  rabss 3205* 
Restricted class abstraction in a subclass relationship. (Contributed
by NM, 16Aug2006.)



Theorem  ssrab 3206* 
Subclass of a restricted class abstraction. (Contributed by NM,
16Aug2006.)



Theorem  ssrabdv 3207* 
Subclass of a restricted class abstraction (deduction form).
(Contributed by NM, 31Aug2006.)



Theorem  rabssdv 3208* 
Subclass of a restricted class abstraction (deduction form).
(Contributed by NM, 2Feb2015.)



Theorem  ss2rabdv 3209* 
Deduction of restricted abstraction subclass from implication.
(Contributed by NM, 30May2006.)



Theorem  ss2rabi 3210 
Inference of restricted abstraction subclass from implication.
(Contributed by NM, 14Oct1999.)



Theorem  rabss2 3211* 
Subclass law for restricted abstraction. (Contributed by NM,
18Dec2004.) (Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  ssab2 3212* 
Subclass relation for the restriction of a class abstraction.
(Contributed by NM, 31Mar1995.)



Theorem  ssrab2 3213* 
Subclass relation for a restricted class. (Contributed by NM,
19Mar1997.)



Theorem  ssrabeq 3214* 
If the restricting class of a restricted class abstraction is a subset
of this restricted class abstraction, it is equal to this restricted
class abstraction. (Contributed by Alexander van der Vekens,
31Dec2017.)



Theorem  rabssab 3215 
A restricted class is a subclass of the corresponding unrestricted class.
(Contributed by Mario Carneiro, 23Dec2016.)



Theorem  uniiunlem 3216* 
A subset relationship useful for converting union to indexed union using
dfiun2 or dfiun2g and intersection to indexed intersection using
dfiin2 . (Contributed by NM, 5Oct2006.) (Proof shortened by Mario
Carneiro, 26Sep2015.)



2.1.13 The difference, union, and intersection
of two classes


2.1.13.1 The difference of two
classes


Theorem  dfdif3 3217* 
Alternate definition of class difference. Definition of relative set
complement in Section 2.3 of [Pierik], p.
10. (Contributed by BJ and
Jim Kingdon, 16Jun2022.)



Theorem  difeq1 3218 
Equality theorem for class difference. (Contributed by NM,
10Feb1997.) (Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  difeq2 3219 
Equality theorem for class difference. (Contributed by NM,
10Feb1997.) (Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  difeq12 3220 
Equality theorem for class difference. (Contributed by FL,
31Aug2009.)



Theorem  difeq1i 3221 
Inference adding difference to the right in a class equality.
(Contributed by NM, 15Nov2002.)



Theorem  difeq2i 3222 
Inference adding difference to the left in a class equality.
(Contributed by NM, 15Nov2002.)



Theorem  difeq12i 3223 
Equality inference for class difference. (Contributed by NM,
29Aug2004.)



Theorem  difeq1d 3224 
Deduction adding difference to the right in a class equality.
(Contributed by NM, 15Nov2002.)



Theorem  difeq2d 3225 
Deduction adding difference to the left in a class equality.
(Contributed by NM, 15Nov2002.)



Theorem  difeq12d 3226 
Equality deduction for class difference. (Contributed by FL,
29May2014.)



Theorem  difeqri 3227* 
Inference from membership to difference. (Contributed by NM,
17May1998.) (Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  nfdif 3228 
Boundvariable hypothesis builder for class difference. (Contributed by
NM, 3Dec2003.) (Revised by Mario Carneiro, 13Oct2016.)



Theorem  eldifi 3229 
Implication of membership in a class difference. (Contributed by NM,
29Apr1994.)



Theorem  eldifn 3230 
Implication of membership in a class difference. (Contributed by NM,
3May1994.)



Theorem  elndif 3231 
A set does not belong to a class excluding it. (Contributed by NM,
27Jun1994.)



Theorem  difdif 3232 
Double class difference. Exercise 11 of [TakeutiZaring] p. 22.
(Contributed by NM, 17May1998.)



Theorem  difss 3233 
Subclass relationship for class difference. Exercise 14 of
[TakeutiZaring] p. 22.
(Contributed by NM, 29Apr1994.)



Theorem  difssd 3234 
A difference of two classes is contained in the minuend. Deduction form
of difss 3233. (Contributed by David Moews, 1May2017.)



Theorem  difss2 3235 
If a class is contained in a difference, it is contained in the minuend.
(Contributed by David Moews, 1May2017.)



Theorem  difss2d 3236 
If a class is contained in a difference, it is contained in the minuend.
Deduction form of difss2 3235. (Contributed by David Moews,
1May2017.)



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



Theorem  ddifnel 3238* 
Double complement under universal class. The hypothesis corresponds to
stability of membership in , which is weaker than decidability
(see dcstab 830). Actually, the conclusion is a
characterization of
stability of membership in a class (see ddifstab 3239) . 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 3345. (Contributed by Jim Kingdon,
21Jul2018.)



Theorem  ddifstab 3239* 
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 3240 
Contraposition law for subsets. (Contributed by NM, 22Mar1998.)



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



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



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



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



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



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



Theorem  raldifb 3247 
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 3248 
Expansion of membership in class union. Theorem 12 of [Suppes] p. 25.
(Contributed by NM, 7Aug1994.)



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



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



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



Theorem  equncom 3252 
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 3253 
Inference form of equncom 3252. (Contributed by Alan Sare,
18Feb2012.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



2.1.13.3 The intersection of two
classes


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



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



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



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



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



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



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



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



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



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



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

