Type  Label  Description 
Statement 

Theorem  indi 3501 
Distributive law for intersection over union. Exercise 10 of
[TakeutiZaring] p. 17.
(Contributed by NM, 30Sep2002.) (Proof
shortened by Andrew Salmon, 26Jun2011.)



Theorem  undi 3502 
Distributive law for union over intersection. Exercise 11 of
[TakeutiZaring] p. 17.
(Contributed by NM, 30Sep2002.) (Proof
shortened by Andrew Salmon, 26Jun2011.)



Theorem  indir 3503 
Distributive law for intersection over union. Theorem 28 of [Suppes]
p. 27. (Contributed by NM, 30Sep2002.)



Theorem  undir 3504 
Distributive law for union over intersection. Theorem 29 of [Suppes]
p. 27. (Contributed by NM, 30Sep2002.)



Theorem  unineq 3505 
Infer equality from equalities of union and intersection. Exercise 20
of [Enderton] p. 32 and its converse.
(Contributed by NM,
10Aug2004.)



Theorem  uneqin 3506 
Equality of union and intersection implies equality of their arguments.
(Contributed by NM, 16Apr2006.) (Proof shortened by Andrew Salmon,
26Jun2011.)



Theorem  difundi 3507 
Distributive law for class difference. Theorem 39 of [Suppes] p. 29.
(Contributed by NM, 17Aug2004.)



Theorem  difundir 3508 
Distributive law for class difference. (Contributed by NM,
17Aug2004.)



Theorem  difindi 3509 
Distributive law for class difference. Theorem 40 of [Suppes] p. 29.
(Contributed by NM, 17Aug2004.)



Theorem  difindir 3510 
Distributive law for class difference. (Contributed by NM,
17Aug2004.)



Theorem  indifdir 3511 
Distribute intersection over difference. (Contributed by Scott Fenton,
14Apr2011.)



Theorem  undm 3512 
De Morgan's law for union. Theorem 5.2(13) of [Stoll] p. 19.
(Contributed by NM, 18Aug2004.)



Theorem  indm 3513 
De Morgan's law for intersection. Theorem 5.2(13') of [Stoll] p. 19.
(Contributed by NM, 18Aug2004.)



Theorem  difun1 3514 
A relationship involving double difference and union. (Contributed by NM,
29Aug2004.)



Theorem  undif3 3515 
An equality involving class union and class difference. The first
equality of Exercise 13 of [TakeutiZaring] p. 22. (Contributed by Alan
Sare, 17Apr2012.)



Theorem  difin2 3516 
Represent a set difference as an intersection with a larger difference.
(Contributed by Jeff Madsen, 2Sep2009.)



Theorem  dif32 3517 
Swap second and third argument of double difference. (Contributed by NM,
18Aug2004.)



Theorem  difabs 3518 
Absorptionlike law for class difference: you can remove a class only
once. (Contributed by FL, 2Aug2009.)



Theorem  symdif1 3519 
Two ways to express symmetric difference. This theorem shows the
equivalence of the definition of symmetric difference in [Stoll] p. 13 and
the restated definition in Example 4.1 of [Stoll] p. 262. (Contributed by
NM, 17Aug2004.)



Theorem  symdif2 3520* 
Two ways to express symmetric difference. (Contributed by NM,
17Aug2004.) (Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  unab 3521 
Union of two class abstractions. (Contributed by NM, 29Sep2002.)
(Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  inab 3522 
Intersection of two class abstractions. (Contributed by NM,
29Sep2002.) (Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  difab 3523 
Difference of two class abstractions. (Contributed by NM,
23Oct2004.) (Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  complab 3524 
Complement of a class abstraction. (Contributed by SF, 12Jan2015.)

∼


Theorem  notab 3525 
A class builder defined by a negation. (Contributed by FL,
18Sep2010.)



Theorem  unrab 3526 
Union of two restricted class abstractions. (Contributed by NM,
25Mar2004.)



Theorem  inrab 3527 
Intersection of two restricted class abstractions. (Contributed by NM,
1Sep2006.)



Theorem  inrab2 3528* 
Intersection with a restricted class abstraction. (Contributed by NM,
19Nov2007.)



Theorem  difrab 3529 
Difference of two restricted class abstractions. (Contributed by NM,
23Oct2004.)



Theorem  dfrab2 3530* 
Alternate definition of restricted class abstraction. (Contributed by
NM, 20Sep2003.)



Theorem  dfrab3 3531* 
Alternate definition of restricted class abstraction. (Contributed by
Mario Carneiro, 8Sep2013.)



Theorem  notrab 3532* 
Complementation of restricted class abstractions. (Contributed by Mario
Carneiro, 3Sep2015.)



Theorem  dfrab3ss 3533* 
Restricted class abstraction with a common superset. (Contributed by
Stefan O'Rear, 12Sep2015.) (Proof shortened by Mario Carneiro,
8Nov2015.)



Theorem  rabun2 3534 
Abstraction restricted to a union. (Contributed by Stefan O'Rear,
5Feb2015.)



Theorem  reuss2 3535* 
Transfer uniqueness to a smaller subclass. (Contributed by NM,
20Oct2005.)



Theorem  reuss 3536* 
Transfer uniqueness to a smaller subclass. (Contributed by NM,
21Aug1999.)



Theorem  reuun1 3537* 
Transfer uniqueness to a smaller class. (Contributed by NM,
21Oct2005.)



Theorem  reuun2 3538* 
Transfer uniqueness to a smaller or larger class. (Contributed by NM,
21Oct2005.)



Theorem  reupick 3539* 
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
NM, 21Aug1999.)



Theorem  reupick3 3540* 
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
Mario Carneiro, 19Nov2016.)



Theorem  reupick2 3541* 
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
Mario Carneiro, 15Dec2013.) (Proof shortened by Mario Carneiro,
19Nov2016.)



Theorem  symdifcom 3542 
Symmetric difference commutes. (Contributed by SF, 11Jan2015.)



Theorem  compleqb 3543 
Two classes are equal iff their complements are equal. (Contributed by
SF, 11Jan2015.)

∼ ∼ 

Theorem  necompl 3544 
A class is not equal to its complement. (Contributed by SF,
11Jan2015.)

∼ 

Theorem  dfin5 3545 
Definition of intersection in terms of union. (Contributed by SF,
12Jan2015.)

∼ ∼ ∼ 

Theorem  dfun4 3546 
Definition of union in terms of intersection. (Contributed by SF,
12Jan2015.)

∼ ∼ ∼ 

Theorem  iunin 3547 
Intersection of two complements is equal to the complement of a union.
(Contributed by SF, 12Jan2015.)

∼
∼ ∼ 

Theorem  iinun 3548 
Complement of intersection is equal to union of complements. (Contributed
by SF, 12Jan2015.)

∼
∼ ∼ 

Theorem  difsscompl 3549 
A difference is a subset of the complement of its second argument.
(Contributed by SF, 10Mar2015.)

∼ 

2.1.13 The empty set


Syntax  c0 3550 
Extend class notation to include the empty set.



Definition  dfnul 3551 
Define the empty set. Special case of Exercise 4.10(o) of [Mendelson]
p. 231. For a more traditional definition, but requiring a dummy
variable, see dfnul2 3552. (Contributed by NM, 5Aug1993.)



Theorem  dfnul2 3552 
Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring]
p. 20. (Contributed by NM, 26Dec1996.)



Theorem  dfnul3 3553 
Alternate definition of the empty set. (Contributed by NM,
25Mar2004.)



Theorem  noel 3554 
The empty set has no elements. Theorem 6.14 of [Quine] p. 44.
(Contributed by NM, 5Aug1993.) (Proof shortened by Mario Carneiro,
1Sep2015.)



Theorem  n0i 3555 
If a set has elements, it is not empty. (Contributed by NM,
31Dec1993.)



Theorem  ne0i 3556 
If a set has elements, it is not empty. (Contributed by NM,
31Dec1993.)



Theorem  vn0 3557 
The universal class is not equal to the empty set. (Contributed by NM,
11Sep2008.)



Theorem  n0f 3558 
A nonempty class has at least one element. Proposition 5.17(1) of
[TakeutiZaring] p. 20. This
version of n0 3559 requires only that
not be free in, rather than not occur in, . (Contributed by NM,
17Oct2003.)



Theorem  n0 3559* 
A nonempty class has at least one element. Proposition 5.17(1) of
[TakeutiZaring] p. 20.
(Contributed by NM, 29Sep2006.)



Theorem  neq0 3560* 
A nonempty class has at least one element. Proposition 5.17(1) of
[TakeutiZaring] p. 20.
(Contributed by NM, 5Aug1993.)



Theorem  reximdva0 3561* 
Restricted existence deduced from nonempty class. (Contributed by NM,
1Feb2012.)



Theorem  n0moeu 3562* 
A case of equivalence of "at most one" and "only one".
(Contributed by
FL, 6Dec2010.)



Theorem  rex0 3563 
Vacuous existential quantification is false. (Contributed by NM,
15Oct2003.)



Theorem  eq0 3564* 
The empty set has no elements. Theorem 2 of [Suppes] p. 22.
(Contributed by NM, 29Aug1993.)



Theorem  eqv 3565* 
The universe contains every set. (Contributed by NM, 11Sep2006.)



Theorem  0el 3566* 
Membership of the empty set in another class. (Contributed by NM,
29Jun2004.)



Theorem  abvor0 3567* 
The class builder of a wff not containing the abstraction variable is
either the universal class or the empty set. (Contributed by Mario
Carneiro, 29Aug2013.)



Theorem  abn0 3568 
Nonempty class abstraction. (Contributed by NM, 26Dec1996.) (Proof
shortened by Mario Carneiro, 11Nov2016.)



Theorem  ab0 3569 
Empty class abstraction. (Contributed by SF, 5Jan2018.)



Theorem  rabn0 3570 
Nonempty restricted class abstraction. (Contributed by NM,
29Aug1999.)



Theorem  rab0 3571 
Any restricted class abstraction restricted to the empty set is empty.
(Contributed by NM, 15Oct2003.) (Proof shortened by Andrew Salmon,
26Jun2011.)



Theorem  rabeq0 3572 
Condition for a restricted class abstraction to be empty. (Contributed by
Jeff Madsen, 7Jun2010.)



Theorem  rabxm 3573* 
Law of excluded middle, in terms of restricted class abstractions.
(Contributed by Jeff Madsen, 20Jun2011.)



Theorem  rabnc 3574* 
Law of noncontradiction, in terms of restricted class abstractions.
(Contributed by Jeff Madsen, 20Jun2011.)



Theorem  un0 3575 
The union of a class with the empty set is itself. Theorem 24 of
[Suppes] p. 27. (Contributed by NM,
5Aug1993.)



Theorem  in0 3576 
The intersection of a class with the empty set is the empty set.
Theorem 16 of [Suppes] p. 26.
(Contributed by NM, 5Aug1993.)



Theorem  inv1 3577 
The intersection of a class with the universal class is itself. Exercise
4.10(k) of [Mendelson] p. 231.
(Contributed by NM, 17May1998.)



Theorem  unv 3578 
The union of a class with the universal class is the universal class.
Exercise 4.10(l) of [Mendelson] p. 231.
(Contributed by NM,
17May1998.)



Theorem  0ss 3579 
The null set is a subset of any class. Part of Exercise 1 of
[TakeutiZaring] p. 22.
(Contributed by NM, 5Aug1993.)



Theorem  ss0b 3580 
Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its
converse. (Contributed by NM, 17Sep2003.)



Theorem  ss0 3581 
Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23.
(Contributed by NM, 13Aug1994.)



Theorem  sseq0 3582 
A subclass of an empty class is empty. (Contributed by NM, 7Mar2007.)
(Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  ssn0 3583 
A class with a nonempty subclass is nonempty. (Contributed by NM,
17Feb2007.)



Theorem  abf 3584 
A class builder with a false argument is empty. (Contributed by NM,
20Jan2012.)



Theorem  eq0rdv 3585* 
Deduction rule for equality to the empty set. (Contributed by NM,
11Jul2014.)



Theorem  un00 3586 
Two classes are empty iff their union is empty. (Contributed by NM,
11Aug2004.)



Theorem  vss 3587 
Only the universal class has the universal class as a subclass.
(Contributed by NM, 17Sep2003.) (Proof shortened by Andrew Salmon,
26Jun2011.)



Theorem  0pss 3588 
The null set is a proper subset of any nonempty set. (Contributed by NM,
27Feb1996.)



Theorem  npss0 3589 
No set is a proper subset of the empty set. (Contributed by NM,
17Jun1998.) (Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  pssv 3590 
Any nonuniversal class is a proper subclass of the universal class.
(Contributed by NM, 17May1998.)



Theorem  disj 3591* 
Two ways of saying that two classes are disjoint (have no members in
common). (Contributed by NM, 17Feb2004.)



Theorem  disjr 3592* 
Two ways of saying that two classes are disjoint. (Contributed by Jeff
Madsen, 19Jun2011.)



Theorem  disj1 3593* 
Two ways of saying that two classes are disjoint (have no members in
common). (Contributed by NM, 19Aug1993.)



Theorem  reldisj 3594 
Two ways of saying that two classes are disjoint, using the complement
of relative
to a universe .
(Contributed by NM,
15Feb2007.) (Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  disj3 3595 
Two ways of saying that two classes are disjoint. (Contributed by NM,
19May1998.)



Theorem  disjne 3596 
Members of disjoint sets are not equal. (Contributed by NM,
28Mar2007.) (Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  disjel 3597 
A set can't belong to both members of disjoint classes. (Contributed by
NM, 28Feb2015.)



Theorem  disj2 3598 
Two ways of saying that two classes are disjoint. (Contributed by NM,
17May1998.)



Theorem  disj4 3599 
Two ways of saying that two classes are disjoint. (Contributed by NM,
21Mar2004.)



Theorem  ssdisj 3600 
Intersection with a subclass of a disjoint class. (Contributed by FL,
24Jan2007.)

