Type  Label  Description 
Statement 

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



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



Theorem  indmss 3303 
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 3304 
A relationship involving double difference and union. (Contributed by NM,
29Aug2004.)



Theorem  undif3ss 3305 
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 3306 
Represent a set difference as an intersection with a larger difference.
(Contributed by Jeff Madsen, 2Sep2009.)



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



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



Theorem  symdif1 3309 
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 3310* 
Expressing symmetric difference with exclusiveor or two differences.
(Contributed by Jim Kingdon, 28Jul2018.)



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



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



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



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



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



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



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



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



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



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



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



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



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



2.1.13.6 Restricted uniqueness with difference,
union, and intersection


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



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



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



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



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



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



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



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



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



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



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



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



Theorem  ne0d 3338 
Deduction form of ne0i 3337. If a class has elements, then it is
nonempty. (Contributed by Glauco Siliprandi, 23Oct2021.)



Theorem  n0ii 3339 
If a class has elements, then it is not empty. Inference associated
with n0i 3336. (Contributed by BJ, 15Jul2021.)



Theorem  ne0ii 3340 
If a class has elements, then it is nonempty. Inference associated with
ne0i 3337. (Contributed by Glauco Siliprandi,
11Dec2019.)



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



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



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



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



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



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



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



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



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



Theorem  notm0 3351* 
A class is not inhabited if and only if it is empty. (Contributed by
Jim Kingdon, 1Jul2022.)



Theorem  nel0 3352* 
From the general negation of membership in , infer that is
the empty set. (Contributed by BJ, 6Oct2018.)



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



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



Theorem  abn0m 3356* 
Inhabited class abstraction. (Contributed by Jim Kingdon,
8Jul2022.)



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



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



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



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



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



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

DECID 

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



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



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



Theorem  0in 3366 
The intersection of the empty set with a class is the empty set.
(Contributed by Glauco Siliprandi, 17Aug2020.)



Theorem  inv1 3367 
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 3368 
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 3369 
The null set is a subset of any class. Part of Exercise 1 of
[TakeutiZaring] p. 22.
(Contributed by NM, 5Aug1993.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  ssdif0im 3395 
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 3396 
Universal class equality in terms of empty difference. (Contributed by
Jim Kingdon, 3Aug2018.)



Theorem  difrab0eqim 3397* 
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  inssdif0im 3398 
Intersection, subclass, and difference relationship. In classical logic
the converse would also hold. (Contributed by Jim Kingdon,
3Aug2018.)



Theorem  difid 3399 
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 3400 
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 3399. (Contributed by David Abernethy,
17Jun2012.) (Proof modification is discouraged.)
(New usage is discouraged.)

