Type  Label  Description 
Statement 

Theorem  nssne1 3001 
Two classes are different if they don't include the same class.
(Contributed by NM, 23Apr2015.)



Theorem  nssne2 3002 
Two classes are different if they are not subclasses of the same class.
(Contributed by NM, 23Apr2015.)



Theorem  nssr 3003* 
Negation of subclass relationship. One direction of Exercise 13 of
[TakeutiZaring] p. 18.
(Contributed by Jim Kingdon, 15Jul2018.)



Theorem  ssralv 3004* 
Quantification restricted to a subclass. (Contributed by NM,
11Mar2006.)



Theorem  ssrexv 3005* 
Existential quantification restricted to a subclass. (Contributed by
NM, 11Jan2007.)



Theorem  ralss 3006* 
Restricted universal quantification on a subset in terms of superset.
(Contributed by Stefan O'Rear, 3Apr2015.)



Theorem  rexss 3007* 
Restricted existential quantification on a subset in terms of superset.
(Contributed by Stefan O'Rear, 3Apr2015.)



Theorem  ss2ab 3008 
Class abstractions in a subclass relationship. (Contributed by NM,
3Jul1994.)



Theorem  abss 3009* 
Class abstraction in a subclass relationship. (Contributed by NM,
16Aug2006.)



Theorem  ssab 3010* 
Subclass of a class abstraction. (Contributed by NM, 16Aug2006.)



Theorem  ssabral 3011* 
The relation for a subclass of a class abstraction is equivalent to
restricted quantification. (Contributed by NM, 6Sep2006.)



Theorem  ss2abi 3012 
Inference of abstraction subclass from implication. (Contributed by NM,
31Mar1995.)



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  ssrabeq 3026* 
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 3027 
A restricted class is a subclass of the corresponding unrestricted class.
(Contributed by Mario Carneiro, 23Dec2016.)



Theorem  uniiunlem 3028* 
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.)



Theorem  dfpss2 3029 
Alternate definition of proper subclass. (Contributed by NM,
7Feb1996.)



Theorem  dfpss3 3030 
Alternate definition of proper subclass. (Contributed by NM, 7Feb1996.)
(Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  psseq1 3031 
Equality theorem for proper subclass. (Contributed by NM, 7Feb1996.)



Theorem  psseq2 3032 
Equality theorem for proper subclass. (Contributed by NM, 7Feb1996.)



Theorem  psseq1i 3033 
An equality inference for the proper subclass relationship.
(Contributed by NM, 9Jun2004.)



Theorem  psseq2i 3034 
An equality inference for the proper subclass relationship.
(Contributed by NM, 9Jun2004.)



Theorem  psseq12i 3035 
An equality inference for the proper subclass relationship.
(Contributed by NM, 9Jun2004.)



Theorem  psseq1d 3036 
An equality deduction for the proper subclass relationship.
(Contributed by NM, 9Jun2004.)



Theorem  psseq2d 3037 
An equality deduction for the proper subclass relationship.
(Contributed by NM, 9Jun2004.)



Theorem  psseq12d 3038 
An equality deduction for the proper subclass relationship.
(Contributed by NM, 9Jun2004.)



Theorem  pssss 3039 
A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23.
(Contributed by NM, 7Feb1996.)



Theorem  pssne 3040 
Two classes in a proper subclass relationship are not equal. (Contributed
by NM, 16Feb2015.)



Theorem  pssssd 3041 
Deduce subclass from proper subclass. (Contributed by NM,
29Feb1996.)



Theorem  pssned 3042 
Proper subclasses are unequal. Deduction form of pssne 3040.
(Contributed by David Moews, 1May2017.)



Theorem  sspssr 3043 
Subclass in terms of proper subclass. (Contributed by Jim Kingdon,
16Jul2018.)



Theorem  pssirr 3044 
Proper subclass is irreflexive. Theorem 7 of [Suppes] p. 23.
(Contributed by NM, 7Feb1996.)



Theorem  pssn2lp 3045 
Proper subclass has no 2cycle loops. Compare Theorem 8 of [Suppes]
p. 23. (Contributed by NM, 7Feb1996.) (Proof shortened by Andrew
Salmon, 26Jun2011.)



Theorem  sspsstrir 3046 
Two ways of stating trichotomy with respect to inclusion. (Contributed by
Jim Kingdon, 16Jul2018.)



Theorem  ssnpss 3047 
Partial trichotomy law for subclasses. (Contributed by NM, 16May1996.)
(Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  sspssn 3048 
Like pssn2lp 3045 but for subset and proper subset.
(Contributed by Jim
Kingdon, 17Jul2018.)



Theorem  psstr 3049 
Transitive law for proper subclass. Theorem 9 of [Suppes] p. 23.
(Contributed by NM, 7Feb1996.)



Theorem  sspsstr 3050 
Transitive law for subclass and proper subclass. (Contributed by NM,
3Apr1996.)



Theorem  psssstr 3051 
Transitive law for subclass and proper subclass. (Contributed by NM,
3Apr1996.)



Theorem  psstrd 3052 
Proper subclass inclusion is transitive. Deduction form of psstr 3049.
(Contributed by David Moews, 1May2017.)



Theorem  sspsstrd 3053 
Transitivity involving subclass and proper subclass inclusion.
Deduction form of sspsstr 3050. (Contributed by David Moews,
1May2017.)



Theorem  psssstrd 3054 
Transitivity involving subclass and proper subclass inclusion.
Deduction form of psssstr 3051. (Contributed by David Moews,
1May2017.)



2.1.13 The difference, union, and intersection
of two classes


2.1.13.1 The difference of two
classes


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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  ddifnel 3075* 
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 3175. (Contributed by Jim
Kingdon, 21Jul2018.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

