Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



2.1.13.3 The intersection of two
classes


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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  dfss5 3194 
Another definition of subclasshood. Similar to dfss 3001, dfss 3002, and
dfss1 3193. (Contributed by David Moews, 1May2017.)



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



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



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



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



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



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

