Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



Theorem  equncom 3410 
If a class equals the union of two other classes, then it equals the union
of those two classes commuted. equncom 3410 was automatically derived from
equncomVD in set.mm using the tools program
translate_without_overwriting.cmd and minimizing. (Contributed by Alan
Sare, 18Feb2012.)



Theorem  equncomi 3411 
Inference form of equncom 3410. equncomi 3411 was automatically derived from
equncomiVD in set.mm using the tools program
translate_without_overwriting.cmd and minimizing. (Contributed by
Alan Sare, 18Feb2012.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  dfss5 3462 
Another definition of subclasshood. Similar to dfss 3260, dfss 3261, and
dfss1 3461. (Contributed by David Moews, 1May2017.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  dfss4 3490 
Subclass defined in terms of class difference. See comments under
dfun2 3491. (Contributed by NM, 22Mar1998.) (Proof
shortened by Andrew
Salmon, 26Jun2011.)



Theorem  dfun2 3491 
An alternate definition of the union of two classes in terms of class
difference, requiring no dummy variables. Along with dfin2 3492 and
dfss4 3490 it shows we can express union, intersection,
and subset directly
in terms of the single "primitive" operation (class difference).
(Contributed by NM, 10Jun2004.)



Theorem  dfin2 3492 
An alternate definition of the intersection of two classes in terms of
class difference, requiring no dummy variables. See comments under
dfun2 3491. Another version is given by dfin4 3496. (Contributed by NM,
10Jun2004.)



Theorem  difin 3493 
Difference with intersection. Theorem 33 of [Suppes] p. 29.
(Contributed by NM, 31Mar1998.) (Proof shortened by Andrew Salmon,
26Jun2011.)



Theorem  dfun3 3494 
Union defined in terms of intersection (De Morgan's law). Definition of
union in [Mendelson] p. 231.
(Contributed by NM, 8Jan2002.)



Theorem  dfin3 3495 
Intersection defined in terms of union (De Morgan's law. Similar to
Exercise 4.10(n) of [Mendelson] p. 231.
(Contributed by NM,
8Jan2002.)



Theorem  dfin4 3496 
Alternate definition of the intersection of two classes. Exercise 4.10(q)
of [Mendelson] p. 231. (Contributed by
NM, 25Nov2003.)



Theorem  invdif 3497 
Intersection with universal complement. Remark in [Stoll] p. 20.
(Contributed by NM, 17Aug2004.)



Theorem  indif 3498 
Intersection with class difference. Theorem 34 of [Suppes] p. 29.
(Contributed by NM, 17Aug2004.)



Theorem  indif2 3499 
Bring an intersection in and out of a class difference. (Contributed by
Jeff Hankins, 15Jul2009.)



Theorem  indif1 3500 
Bring an intersection in and out of a class difference. (Contributed by
Mario Carneiro, 15May2015.)

