Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

DECID 

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



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



Theorem  in0 3424 
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 3425 
The intersection of the empty set with a class is the empty set.
(Contributed by Glauco Siliprandi, 17Aug2020.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  difin0 3463 
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 3464 
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 3465 
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 3466 
Absorption of difference by union. (Contributed by NM, 18Aug2013.)



Theorem  inundifss 3467 
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  disjdif2 3468 
The difference of a class and a class disjoint from it is the original
class. (Contributed by BJ, 21Apr2019.)



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



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



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



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



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



Theorem  difdifdirss 3474 
Distributive law for class difference. In classical logic, as in Exercise
4.8 of [Stoll] p. 16, this would be equality
rather than subset.
(Contributed by Jim Kingdon, 4Aug2018.)



Theorem  uneqdifeqim 3475 
Two ways that and
can
"partition"
(when and
don't overlap and is a part of ). In classical logic, the
second implication would be a biconditional. (Contributed by Jim Kingdon,
4Aug2018.)



Theorem  r19.2m 3476* 
Theorem 19.2 of [Margaris] p. 89 with
restricted quantifiers (compare
19.2 1615). The restricted version is valid only when
the domain of
quantification is inhabited. (Contributed by Jim Kingdon, 5Aug2018.)
(Revised by Jim Kingdon, 7Apr2023.)



Theorem  r19.2mOLD 3477* 
Theorem 19.2 of [Margaris] p. 89 with
restricted quantifiers (compare
19.2 1615). The restricted version is valid only when
the domain of
quantification is inhabited. (Contributed by Jim Kingdon, 5Aug2018.)
Obsolete version of r19.2m 3476 as of 7Apr2023.
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  r19.3rm 3478* 
Restricted quantification of wff not containing quantified variable.
(Contributed by Jim Kingdon, 19Dec2018.)



Theorem  r19.28m 3479* 
Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It
is valid only when the domain of quantification is inhabited.
(Contributed by Jim Kingdon, 5Aug2018.)



Theorem  r19.3rmv 3480* 
Restricted quantification of wff not containing quantified variable.
(Contributed by Jim Kingdon, 6Aug2018.)



Theorem  r19.9rmv 3481* 
Restricted quantification of wff not containing quantified variable.
(Contributed by Jim Kingdon, 5Aug2018.)



Theorem  r19.28mv 3482* 
Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It
is valid only when the domain of quantification is inhabited.
(Contributed by Jim Kingdon, 6Aug2018.)



Theorem  r19.45mv 3483* 
Restricted version of Theorem 19.45 of [Margaris] p. 90. (Contributed
by NM, 27May1998.)



Theorem  r19.44mv 3484* 
Restricted version of Theorem 19.44 of [Margaris] p. 90. (Contributed
by NM, 27May1998.)



Theorem  r19.27m 3485* 
Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It
is valid only when the domain of quantification is inhabited.
(Contributed by Jim Kingdon, 5Aug2018.)



Theorem  r19.27mv 3486* 
Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It
is valid only when the domain of quantification is inhabited.
(Contributed by Jim Kingdon, 5Aug2018.)



Theorem  rzal 3487* 
Vacuous quantification is always true. (Contributed by NM,
11Mar1997.) (Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  rexn0 3488* 
Restricted existential quantification implies its restriction is
nonempty (it is also inhabited as shown in rexm 3489). (Contributed by
Szymon Jaroszewicz, 3Apr2007.)



Theorem  rexm 3489* 
Restricted existential quantification implies its restriction is
inhabited. (Contributed by Jim Kingdon, 16Oct2018.)



Theorem  ralidm 3490* 
Idempotent law for restricted quantifier. (Contributed by NM,
28Mar1997.)



Theorem  ral0 3491 
Vacuous universal quantification is always true. (Contributed by NM,
20Oct2005.)



Theorem  rgenm 3492* 
Generalization rule that eliminates an inhabited class requirement.
(Contributed by Jim Kingdon, 5Aug2018.)



Theorem  ralf0 3493* 
The quantification of a falsehood is vacuous when true. (Contributed by
NM, 26Nov2005.)



Theorem  ralm 3494 
Inhabited classes and restricted quantification. (Contributed by Jim
Kingdon, 6Aug2018.)



Theorem  raaanlem 3495* 
Special case of raaan 3496 where is inhabited. (Contributed by Jim
Kingdon, 6Aug2018.)



Theorem  raaan 3496* 
Rearrange restricted quantifiers. (Contributed by NM, 26Oct2010.)



Theorem  raaanv 3497* 
Rearrange restricted quantifiers. (Contributed by NM, 11Mar1997.)



Theorem  sbss 3498* 
Set substitution into the first argument of a subset relation.
(Contributed by Rodolfo Medina, 7Jul2010.) (Proof shortened by Mario
Carneiro, 14Nov2016.)



Theorem  sbcssg 3499 
Distribute proper substitution through a subclass relation.
(Contributed by Alan Sare, 22Jul2012.) (Proof shortened by Alexander
van der Vekens, 23Jul2017.)



Theorem  dcun 3500 
The union of two decidable classes is decidable. (Contributed by Jim
Kingdon, 5Oct2022.)

DECID
DECID
DECID
