Type  Label  Description 
Statement 

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



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



Theorem  ddifnel 3103* 
Double complement under universal class. The hypothesis is one way of
expressing the idea that membership in is decidable. 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 3203. (Contributed by Jim
Kingdon, 21Jul2018.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



2.1.13.3 The intersection of two
classes


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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  dfss5 3170 
Another definition of subclasshood. Similar to dfss 2959, dfss 2960, and
dfss1 3169. (Contributed by David Moews, 1May2017.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  inss1 3185 
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 3186 
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 3187 
Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26.
(Contributed by NM, 15Jun2004.) (Proof shortened by Andrew Salmon,
26Jun2011.)



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



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



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



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



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



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



Theorem  inss 3194 
Inclusion of an intersection of two classes. (Contributed by NM,
30Oct2014.)



2.1.13.4 Combinations of difference, union, and
intersection of two classes


Theorem  unabs 3195 
Absorption law for union. (Contributed by NM, 16Apr2006.)



Theorem  inabs 3196 
Absorption law for intersection. (Contributed by NM, 16Apr2006.)



Theorem  nssinpss 3197 
Negation of subclass expressed in terms of intersection and proper
subclass. (Contributed by NM, 30Jun2004.) (Proof shortened by Andrew
Salmon, 26Jun2011.)



Theorem  nsspssun 3198 
Negation of subclass expressed in terms of proper subclass and union.
(Contributed by NM, 15Sep2004.)



Theorem  ssddif 3199 
Double complement and subset. Similar to ddifss 3203 but inside a class
instead of the
universal class .
In classical logic the
subset operation on the right hand side could be an equality (that is,
).
(Contributed by Jim Kingdon,
24Jul2018.)



Theorem  unssdif 3200 
Union of two classes and class difference. In classical logic this
would be an equality. (Contributed by Jim Kingdon, 24Jul2018.)

