Type  Label  Description 
Statement 

Theorem  eqsstri 3301 
Substitution of equality into a subclass relationship. (Contributed by
NM, 16Jul1995.)



Theorem  eqsstr3i 3302 
Substitution of equality into a subclass relationship. (Contributed by
NM, 19Oct1999.)



Theorem  sseqtri 3303 
Substitution of equality into a subclass relationship. (Contributed by
NM, 28Jul1995.)



Theorem  sseqtr4i 3304 
Substitution of equality into a subclass relationship. (Contributed by
NM, 4Apr1995.)



Theorem  eqsstrd 3305 
Substitution of equality into a subclass relationship. (Contributed by
NM, 25Apr2004.)



Theorem  eqsstr3d 3306 
Substitution of equality into a subclass relationship. (Contributed by
NM, 25Apr2004.)



Theorem  sseqtrd 3307 
Substitution of equality into a subclass relationship. (Contributed by
NM, 25Apr2004.)



Theorem  sseqtr4d 3308 
Substitution of equality into a subclass relationship. (Contributed by
NM, 25Apr2004.)



Theorem  3sstr3i 3309 
Substitution of equality in both sides of a subclass relationship.
(Contributed by NM, 13Jan1996.) (Proof shortened by Eric Schmidt,
26Jan2007.)



Theorem  3sstr4i 3310 
Substitution of equality in both sides of a subclass relationship.
(Contributed by NM, 13Jan1996.) (Proof shortened by Eric Schmidt,
26Jan2007.)



Theorem  3sstr3g 3311 
Substitution of equality into both sides of a subclass relationship.
(Contributed by NM, 1Oct2000.)



Theorem  3sstr4g 3312 
Substitution of equality into both sides of a subclass relationship.
(Contributed by NM, 16Aug1994.) (Proof shortened by Eric Schmidt,
26Jan2007.)



Theorem  3sstr3d 3313 
Substitution of equality into both sides of a subclass relationship.
(Contributed by NM, 1Oct2000.)



Theorem  3sstr4d 3314 
Substitution of equality into both sides of a subclass relationship.
(Contributed by NM, 30Nov1995.) (Proof shortened by Eric Schmidt,
26Jan2007.)



Theorem  syl5eqss 3315 
B chained subclass and equality deduction. (Contributed by NM,
25Apr2004.)



Theorem  syl5eqssr 3316 
B chained subclass and equality deduction. (Contributed by NM,
25Apr2004.)



Theorem  syl6sseq 3317 
A chained subclass and equality deduction. (Contributed by NM,
25Apr2004.)



Theorem  syl6sseqr 3318 
A chained subclass and equality deduction. (Contributed by NM,
25Apr2004.)



Theorem  syl5sseq 3319 
Subclass transitivity deduction. (Contributed by Jonathan BenNaim,
3Jun2011.)



Theorem  syl5sseqr 3320 
Subclass transitivity deduction. (Contributed by Jonathan BenNaim,
3Jun2011.)



Theorem  syl6eqss 3321 
A chained subclass and equality deduction. (Contributed by Mario
Carneiro, 2Jan2017.)



Theorem  syl6eqssr 3322 
A chained subclass and equality deduction. (Contributed by Mario
Carneiro, 2Jan2017.)



Theorem  eqimss 3323 
Equality implies the subclass relation. (Contributed by NM, 5Aug1993.)
(Proof shortened by Andrew Salmon, 21Jun2011.)



Theorem  eqimss2 3324 
Equality implies the subclass relation. (Contributed by NM,
23Nov2003.)



Theorem  eqimssi 3325 
Infer subclass relationship from equality. (Contributed by NM,
6Jan2007.)



Theorem  eqimss2i 3326 
Infer subclass relationship from equality. (Contributed by NM,
7Jan2007.)



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



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



Theorem  nss 3329* 
Negation of subclass relationship. Exercise 13 of [TakeutiZaring]
p. 18. (Contributed by NM, 25Feb1996.) (Proof shortened by Andrew
Salmon, 21Jun2011.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  sspss 3368 
Subclass in terms of proper subclass. (Contributed by NM,
25Feb1996.)



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



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



Theorem  sspsstri 3371 
Two ways of stating trichotomy with respect to inclusion. (Contributed by
NM, 12Aug2004.)



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



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



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



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



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



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



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



Theorem  npss 3379 
A class is not a proper subclass of another iff it satisfies a
onedirectional form of eqss 3287. (Contributed by Mario Carneiro,
15May2015.)



2.1.12 The difference, union, and intersection
of two classes


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



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



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



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



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



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



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



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



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



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



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



Theorem  neldif 3391 
Implication of membership in a class difference. (Contributed by NM,
28Jun1994.)



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



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



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



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



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



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



Theorem  ddif 3398 
Double complement under universal class. Exercise 4.10(s) of
[Mendelson] p. 231. (Contributed by
NM, 8Jan2002.)



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



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

