Type  Label  Description 
Statement 

Theorem  unssin 3201 
Union as a subset of class complement and intersection (De Morgan's
law). One direction of the definition of union in [Mendelson] p. 231.
This would be an equality, rather than subset, in classical logic.
(Contributed by Jim Kingdon, 25Jul2018.)



Theorem  inssun 3202 
Intersection in terms of class difference and union (De Morgan's law).
Similar to Exercise 4.10(n) of [Mendelson] p. 231. This would be an
equality, rather than subset, in classical logic. (Contributed by Jim
Kingdon, 25Jul2018.)



Theorem  inssddif 3203 
Intersection of two classes and class difference. In classical logic,
such as Exercise 4.10(q) of [Mendelson]
p. 231, this is an equality rather
than subset. (Contributed by Jim Kingdon, 26Jul2018.)



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



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



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



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



Theorem  indifcom 3208 
Commutation law for intersection and difference. (Contributed by Scott
Fenton, 18Feb2013.)



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



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



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



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



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



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



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



Theorem  difindiss 3216 
Distributive law for class difference. In classical logic, for example,
theorem 40 of [Suppes] p. 29, this is an
equality instead of subset.
(Contributed by Jim Kingdon, 26Jul2018.)



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



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



Theorem  difdif2ss 3219 
Set difference with a set difference. In classical logic this would be
equality rather than subset. (Contributed by Jim Kingdon,
27Jul2018.)



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



Theorem  indmss 3221 
De Morgan's law for intersection. In classical logic, this would be
equality rather than subset, as in Theorem 5.2(13') of [Stoll] p. 19.
(Contributed by Jim Kingdon, 27Jul2018.)



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



Theorem  undif3ss 3223 
A subset relationship involving class union and class difference. In
classical logic, this would be equality rather than subset, as in the
first equality of Exercise 13 of [TakeutiZaring] p. 22. (Contributed by
Jim Kingdon, 28Jul2018.)



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



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



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



Theorem  symdif1 3227 
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.)



2.1.13.5 Class abstractions with difference,
union, and intersection of two classes


Theorem  symdifxor 3228* 
Expressing symmetric difference with exclusiveor or two differences.
(Contributed by Jim Kingdon, 28Jul2018.)



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



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



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



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



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



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



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



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



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



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



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



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



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



2.1.13.6 Restricted uniqueness with difference,
union, and intersection


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



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



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



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



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



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



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



2.1.14 The empty set


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



Definition  dfnul 3250 
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 3251. (Contributed by NM, 5Aug1993.)



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



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



Theorem  noel 3253 
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 3254 
If a set has elements, it is not empty. A set with elements is also
inhabited, see elex2 2585. (Contributed by NM, 31Dec1993.)



Theorem  ne0i 3255 
If a set has elements, it is not empty. A set with elements is also
inhabited, see elex2 2585. (Contributed by NM, 31Dec1993.)



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



Theorem  vn0m 3257 
The universal class is inhabited. (Contributed by Jim Kingdon,
17Dec2018.)



Theorem  n0rf 3258 
An inhabited class is nonempty. Following the Definition of [Bauer],
p. 483, we call a class nonempty if and inhabited
if
it has at least one element. In classical logic these two concepts are
equivalent, for example see Proposition 5.17(1) of [TakeutiZaring]
p. 20. This version of n0r 3259 requires only that not be free in,
rather than not occur in, . (Contributed by Jim Kingdon,
31Jul2018.)



Theorem  n0r 3259* 
An inhabited class is nonempty. See n0rf 3258 for more discussion.
(Contributed by Jim Kingdon, 31Jul2018.)



Theorem  neq0r 3260* 
An inhabited class is nonempty. See n0rf 3258 for more discussion.
(Contributed by Jim Kingdon, 31Jul2018.)



Theorem  reximdva0m 3261* 
Restricted existence deduced from inhabited class. (Contributed by Jim
Kingdon, 31Jul2018.)



Theorem  n0mmoeu 3262* 
A case of equivalence of "at most one" and "only one". If
a class is
inhabited, that class having at most one element is equivalent to it
having only one element. (Contributed by Jim Kingdon, 31Jul2018.)



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



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



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



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



Theorem  abvor0dc 3267* 
The class builder of a decidable proposition not containing the
abstraction variable is either the universal class or the empty set.
(Contributed by Jim Kingdon, 1Aug2018.)

DECID 

Theorem  abn0r 3268 
Nonempty class abstraction. (Contributed by Jim Kingdon,
1Aug2018.)



Theorem  rabn0r 3269 
Nonempty restricted class abstraction. (Contributed by Jim Kingdon,
1Aug2018.)



Theorem  rabn0m 3270* 
Inhabited restricted class abstraction. (Contributed by Jim Kingdon,
18Sep2018.)



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



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



Theorem  abeq0 3273 
Condition for a class abstraction to be empty. (Contributed by Jim
Kingdon, 12Aug2018.)



Theorem  rabxmdc 3274* 
Law of excluded middle given decidability, in terms of restricted class
abstractions. (Contributed by Jim Kingdon, 2Aug2018.)

DECID 

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



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



Theorem  in0 3277 
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 3278 
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 3279 
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 3280 
The null set is a subset of any class. Part of Exercise 1 of
[TakeutiZaring] p. 22.
(Contributed by NM, 5Aug1993.)



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



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



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



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



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



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



Theorem  csbprc 3287 
The proper substitution of a proper class for a set into a class results
in the empty set. (Contributed by NM, 17Aug2018.)



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



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



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



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



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



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



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



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



Theorem  reldisj 3296 
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 3297 
Two ways of saying that two classes are disjoint. (Contributed by NM,
19May1998.)



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



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



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

