Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



2.1.13.6 Restricted uniqueness with difference,
union, and intersection


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



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



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



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



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



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



Theorem  reupick2 3217* 
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 3218 
Extend class notation to include the empty set.



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



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



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



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



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



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



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



Theorem  n0rf 3227 
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 3228 requires only that not be free in,
rather than not occur in, . (Contributed by Jim Kingdon,
31Jul2018.)



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



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



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



Theorem  n0mmoeu 3231* 
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 3232 
Vacuous existential quantification is false. (Contributed by NM,
15Oct2003.)



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



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



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



Theorem  abvor0dc 3236* 
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 3237 
Nonempty class abstraction. (Contributed by Jim Kingdon,
1Aug2018.)



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



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



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



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



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



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

DECID 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  disj4im 3270 
A consequence of two classes being disjoint. In classical logic this
would be a biconditional. (Contributed by Jim Kingdon, 2Aug2018.)



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



Theorem  disjpss 3272 
A class is a proper subset of its union with a disjoint nonempty class.
(Contributed by NM, 15Sep2004.)



Theorem  undisj1 3273 
The union of disjoint classes is disjoint. (Contributed by NM,
26Sep2004.)



Theorem  undisj2 3274 
The union of disjoint classes is disjoint. (Contributed by NM,
13Sep2004.)



Theorem  ssindif0im 3275 
Subclass implies empty intersection with difference from the universal
class. (Contributed by NM, 17Sep2003.)



Theorem  inelcm 3276 
The intersection of classes with a common member is nonempty.
(Contributed by NM, 7Apr1994.)



Theorem  minel 3277 
A minimum element of a class has no elements in common with the class.
(Contributed by NM, 22Jun1994.)



Theorem  undif4 3278 
Distribute union over difference. (Contributed by NM, 17May1998.)
(Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  disjssun 3279 
Subset relation for disjoint classes. (Contributed by NM,
25Oct2005.) (Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  ssdif0im 3280 
Subclass implies empty difference. One direction of Exercise 7 of
[TakeutiZaring] p. 22. In
classical logic this would be an
equivalence. (Contributed by Jim Kingdon, 2Aug2018.)



Theorem  vdif0im 3281 
Universal class equality in terms of empty difference. (Contributed by
Jim Kingdon, 3Aug2018.)



Theorem  difrab0eqim 3282* 
If the difference between the restricting class of a restricted class
abstraction and the restricted class abstraction is empty, the
restricting class is equal to this restricted class abstraction.
(Contributed by Jim Kingdon, 3Aug2018.)



Theorem  ssnelpss 3283 
A subclass missing a member is a proper subclass. (Contributed by NM,
12Jan2002.)



Theorem  ssnelpssd 3284 
Subclass inclusion with one element of the superclass missing is proper
subclass inclusion. Deduction form of ssnelpss 3283. (Contributed by
David Moews, 1May2017.)



Theorem  inssdif0im 3285 
Intersection, subclass, and difference relationship. In classical logic
the converse would also hold. (Contributed by Jim Kingdon,
3Aug2018.)



Theorem  difid 3286 
The difference between a class and itself is the empty set. Proposition
5.15 of [TakeutiZaring] p. 20. Also
Theorem 32 of [Suppes] p. 28.
(Contributed by NM, 22Apr2004.)



Theorem  difidALT 3287 
The difference between a class and itself is the empty set. Proposition
5.15 of [TakeutiZaring] p. 20.
Also Theorem 32 of [Suppes] p. 28.
Alternate proof of difid 3286. (Contributed by David Abernethy,
17Jun2012.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  dif0 3288 
The difference between a class and the empty set. Part of Exercise 4.4 of
[Stoll] p. 16. (Contributed by NM,
17Aug2004.)



Theorem  0dif 3289 
The difference between the empty set and a class. Part of Exercise 4.4 of
[Stoll] p. 16. (Contributed by NM,
17Aug2004.)



Theorem  disjdif 3290 
A class and its relative complement are disjoint. Theorem 38 of [Suppes]
p. 29. (Contributed by NM, 24Mar1998.)



Theorem  difin0 3291 
The difference of a class from its intersection is empty. Theorem 37 of
[Suppes] p. 29. (Contributed by NM,
17Aug2004.) (Proof shortened by
Andrew Salmon, 26Jun2011.)



Theorem  undif1ss 3292 
Absorption of difference by union. In classical logic, as Theorem 35 of
[Suppes] p. 29, this would be equality
rather than subset. (Contributed
by Jim Kingdon, 4Aug2018.)



Theorem  undif2ss 3293 
Absorption of difference by union. In classical logic, as in Part of
proof of Corollary 6K of [Enderton] p.
144, this would be equality rather
than subset. (Contributed by Jim Kingdon, 4Aug2018.)



Theorem  undifabs 3294 
Absorption of difference by union. (Contributed by NM, 18Aug2013.)



Theorem  inundifss 3295 
The intersection and class difference of a class with another class are
contained in the original class. In classical logic we'd be able to make
a stronger statement: that everything in the original class is in the
intersection or the difference (that is, this theorem would be equality
rather than subset). (Contributed by Jim Kingdon, 4Aug2018.)



Theorem  difun2 3296 
Absorption of union by difference. Theorem 36 of [Suppes] p. 29.
(Contributed by NM, 19May1998.)



Theorem  undifss 3297 
Union of complementary parts into whole. (Contributed by Jim Kingdon,
4Aug2018.)



Theorem  ssdifin0 3298 
A subset of a difference does not intersect the subtrahend. (Contributed
by Jeff Hankins, 1Sep2013.) (Proof shortened by Mario Carneiro,
24Aug2015.)



Theorem  ssdifeq0 3299 
A class is a subclass of itself subtracted from another iff it is the
empty set. (Contributed by Steve Rodriguez, 20Nov2015.)



Theorem  ssundifim 3300 
A consequence of inclusion in the union of two classes. In classical
logic this would be a biconditional. (Contributed by Jim Kingdon,
4Aug2018.)

