Theorem List for Intuitionistic Logic Explorer - 3301-3400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | difindir 3301 |
Distributive law for class difference. (Contributed by NM,
17-Aug-2004.)
|
|
|
Theorem | indifdir 3302 |
Distribute intersection over difference. (Contributed by Scott Fenton,
14-Apr-2011.)
|
|
|
Theorem | difdif2ss 3303 |
Set difference with a set difference. In classical logic this would be
equality rather than subset. (Contributed by Jim Kingdon,
27-Jul-2018.)
|
|
|
Theorem | undm 3304 |
De Morgan's law for union. Theorem 5.2(13) of [Stoll] p. 19.
(Contributed by NM, 18-Aug-2004.)
|
|
|
Theorem | indmss 3305 |
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, 27-Jul-2018.)
|
|
|
Theorem | difun1 3306 |
A relationship involving double difference and union. (Contributed by NM,
29-Aug-2004.)
|
|
|
Theorem | undif3ss 3307 |
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, 28-Jul-2018.)
|
|
|
Theorem | difin2 3308 |
Represent a set difference as an intersection with a larger difference.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | dif32 3309 |
Swap second and third argument of double difference. (Contributed by NM,
18-Aug-2004.)
|
|
|
Theorem | difabs 3310 |
Absorption-like law for class difference: you can remove a class only
once. (Contributed by FL, 2-Aug-2009.)
|
|
|
Theorem | symdif1 3311 |
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, 17-Aug-2004.)
|
|
|
2.1.13.5 Class abstractions with difference,
union, and intersection of two classes
|
|
Theorem | symdifxor 3312* |
Expressing symmetric difference with exclusive-or or two differences.
(Contributed by Jim Kingdon, 28-Jul-2018.)
|
|
|
Theorem | unab 3313 |
Union of two class abstractions. (Contributed by NM, 29-Sep-2002.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | inab 3314 |
Intersection of two class abstractions. (Contributed by NM,
29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | difab 3315 |
Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | notab 3316 |
A class builder defined by a negation. (Contributed by FL,
18-Sep-2010.)
|
|
|
Theorem | unrab 3317 |
Union of two restricted class abstractions. (Contributed by NM,
25-Mar-2004.)
|
|
|
Theorem | inrab 3318 |
Intersection of two restricted class abstractions. (Contributed by NM,
1-Sep-2006.)
|
|
|
Theorem | inrab2 3319* |
Intersection with a restricted class abstraction. (Contributed by NM,
19-Nov-2007.)
|
|
|
Theorem | difrab 3320 |
Difference of two restricted class abstractions. (Contributed by NM,
23-Oct-2004.)
|
|
|
Theorem | dfrab2 3321* |
Alternate definition of restricted class abstraction. (Contributed by
NM, 20-Sep-2003.)
|
|
|
Theorem | dfrab3 3322* |
Alternate definition of restricted class abstraction. (Contributed by
Mario Carneiro, 8-Sep-2013.)
|
|
|
Theorem | notrab 3323* |
Complementation of restricted class abstractions. (Contributed by Mario
Carneiro, 3-Sep-2015.)
|
|
|
Theorem | dfrab3ss 3324* |
Restricted class abstraction with a common superset. (Contributed by
Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro,
8-Nov-2015.)
|
|
|
Theorem | rabun2 3325 |
Abstraction restricted to a union. (Contributed by Stefan O'Rear,
5-Feb-2015.)
|
|
|
2.1.13.6 Restricted uniqueness with difference,
union, and intersection
|
|
Theorem | reuss2 3326* |
Transfer uniqueness to a smaller subclass. (Contributed by NM,
20-Oct-2005.)
|
|
|
Theorem | reuss 3327* |
Transfer uniqueness to a smaller subclass. (Contributed by NM,
21-Aug-1999.)
|
|
|
Theorem | reuun1 3328* |
Transfer uniqueness to a smaller class. (Contributed by NM,
21-Oct-2005.)
|
|
|
Theorem | reuun2 3329* |
Transfer uniqueness to a smaller or larger class. (Contributed by NM,
21-Oct-2005.)
|
|
|
Theorem | reupick 3330* |
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
NM, 21-Aug-1999.)
|
|
|
Theorem | reupick3 3331* |
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
Mario Carneiro, 19-Nov-2016.)
|
|
|
Theorem | reupick2 3332* |
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
Mario Carneiro, 15-Dec-2013.) (Proof shortened by Mario Carneiro,
19-Nov-2016.)
|
|
|
2.1.14 The empty set
|
|
Syntax | c0 3333 |
Extend class notation to include the empty set.
|
|
|
Definition | df-nul 3334 |
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 3335. (Contributed by NM, 5-Aug-1993.)
|
|
|
Theorem | dfnul2 3335 |
Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring]
p. 20. (Contributed by NM, 26-Dec-1996.)
|
|
|
Theorem | dfnul3 3336 |
Alternate definition of the empty set. (Contributed by NM,
25-Mar-2004.)
|
|
|
Theorem | noel 3337 |
The empty set has no elements. Theorem 6.14 of [Quine] p. 44.
(Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro,
1-Sep-2015.)
|
|
|
Theorem | n0i 3338 |
If a set has elements, it is not empty. A set with elements is also
inhabited, see elex2 2676. (Contributed by NM, 31-Dec-1993.)
|
|
|
Theorem | ne0i 3339 |
If a set has elements, it is not empty. A set with elements is also
inhabited, see elex2 2676. (Contributed by NM, 31-Dec-1993.)
|
|
|
Theorem | ne0d 3340 |
Deduction form of ne0i 3339. If a class has elements, then it is
nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|
|
|
Theorem | n0ii 3341 |
If a class has elements, then it is not empty. Inference associated
with n0i 3338. (Contributed by BJ, 15-Jul-2021.)
|
|
|
Theorem | ne0ii 3342 |
If a class has elements, then it is nonempty. Inference associated with
ne0i 3339. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
|
|
Theorem | vn0 3343 |
The universal class is not equal to the empty set. (Contributed by NM,
11-Sep-2008.)
|
|
|
Theorem | vn0m 3344 |
The universal class is inhabited. (Contributed by Jim Kingdon,
17-Dec-2018.)
|
|
|
Theorem | n0rf 3345 |
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 3346 requires only that not be free in,
rather than not occur in, . (Contributed by Jim Kingdon,
31-Jul-2018.)
|
|
|
Theorem | n0r 3346* |
An inhabited class is nonempty. See n0rf 3345 for more discussion.
(Contributed by Jim Kingdon, 31-Jul-2018.)
|
|
|
Theorem | neq0r 3347* |
An inhabited class is nonempty. See n0rf 3345 for more discussion.
(Contributed by Jim Kingdon, 31-Jul-2018.)
|
|
|
Theorem | reximdva0m 3348* |
Restricted existence deduced from inhabited class. (Contributed by Jim
Kingdon, 31-Jul-2018.)
|
|
|
Theorem | n0mmoeu 3349* |
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, 31-Jul-2018.)
|
|
|
Theorem | rex0 3350 |
Vacuous existential quantification is false. (Contributed by NM,
15-Oct-2003.)
|
|
|
Theorem | eq0 3351* |
The empty set has no elements. Theorem 2 of [Suppes] p. 22.
(Contributed by NM, 29-Aug-1993.)
|
|
|
Theorem | eqv 3352* |
The universe contains every set. (Contributed by NM, 11-Sep-2006.)
|
|
|
Theorem | notm0 3353* |
A class is not inhabited if and only if it is empty. (Contributed by
Jim Kingdon, 1-Jul-2022.)
|
|
|
Theorem | nel0 3354* |
From the general negation of membership in , infer that is
the empty set. (Contributed by BJ, 6-Oct-2018.)
|
|
|
Theorem | 0el 3355* |
Membership of the empty set in another class. (Contributed by NM,
29-Jun-2004.)
|
|
|
Theorem | abvor0dc 3356* |
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, 1-Aug-2018.)
|
DECID |
|
Theorem | abn0r 3357 |
Nonempty class abstraction. (Contributed by Jim Kingdon, 1-Aug-2018.)
|
|
|
Theorem | abn0m 3358* |
Inhabited class abstraction. (Contributed by Jim Kingdon,
8-Jul-2022.)
|
|
|
Theorem | rabn0r 3359 |
Nonempty restricted class abstraction. (Contributed by Jim Kingdon,
1-Aug-2018.)
|
|
|
Theorem | rabn0m 3360* |
Inhabited restricted class abstraction. (Contributed by Jim Kingdon,
18-Sep-2018.)
|
|
|
Theorem | rab0 3361 |
Any restricted class abstraction restricted to the empty set is empty.
(Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon,
26-Jun-2011.)
|
|
|
Theorem | rabeq0 3362 |
Condition for a restricted class abstraction to be empty. (Contributed
by Jeff Madsen, 7-Jun-2010.)
|
|
|
Theorem | abeq0 3363 |
Condition for a class abstraction to be empty. (Contributed by Jim
Kingdon, 12-Aug-2018.)
|
|
|
Theorem | rabxmdc 3364* |
Law of excluded middle given decidability, in terms of restricted class
abstractions. (Contributed by Jim Kingdon, 2-Aug-2018.)
|
DECID |
|
Theorem | rabnc 3365* |
Law of noncontradiction, in terms of restricted class abstractions.
(Contributed by Jeff Madsen, 20-Jun-2011.)
|
|
|
Theorem | un0 3366 |
The union of a class with the empty set is itself. Theorem 24 of
[Suppes] p. 27. (Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | in0 3367 |
The intersection of a class with the empty set is the empty set.
Theorem 16 of [Suppes] p. 26.
(Contributed by NM, 5-Aug-1993.)
|
|
|
Theorem | 0in 3368 |
The intersection of the empty set with a class is the empty set.
(Contributed by Glauco Siliprandi, 17-Aug-2020.)
|
|
|
Theorem | inv1 3369 |
The intersection of a class with the universal class is itself. Exercise
4.10(k) of [Mendelson] p. 231.
(Contributed by NM, 17-May-1998.)
|
|
|
Theorem | unv 3370 |
The union of a class with the universal class is the universal class.
Exercise 4.10(l) of [Mendelson] p. 231.
(Contributed by NM,
17-May-1998.)
|
|
|
Theorem | 0ss 3371 |
The null set is a subset of any class. Part of Exercise 1 of
[TakeutiZaring] p. 22.
(Contributed by NM, 5-Aug-1993.)
|
|
|
Theorem | ss0b 3372 |
Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its
converse. (Contributed by NM, 17-Sep-2003.)
|
|
|
Theorem | ss0 3373 |
Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23.
(Contributed by NM, 13-Aug-1994.)
|
|
|
Theorem | sseq0 3374 |
A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | ssn0 3375 |
A class with a nonempty subclass is nonempty. (Contributed by NM,
17-Feb-2007.)
|
|
|
Theorem | abf 3376 |
A class builder with a false argument is empty. (Contributed by NM,
20-Jan-2012.)
|
|
|
Theorem | eq0rdv 3377* |
Deduction for equality to the empty set. (Contributed by NM,
11-Jul-2014.)
|
|
|
Theorem | csbprc 3378 |
The proper substitution of a proper class for a set into a class results
in the empty set. (Contributed by NM, 17-Aug-2018.)
|
|
|
Theorem | un00 3379 |
Two classes are empty iff their union is empty. (Contributed by NM,
11-Aug-2004.)
|
|
|
Theorem | vss 3380 |
Only the universal class has the universal class as a subclass.
(Contributed by NM, 17-Sep-2003.) (Proof shortened by Andrew Salmon,
26-Jun-2011.)
|
|
|
Theorem | disj 3381* |
Two ways of saying that two classes are disjoint (have no members in
common). (Contributed by NM, 17-Feb-2004.)
|
|
|
Theorem | disjr 3382* |
Two ways of saying that two classes are disjoint. (Contributed by Jeff
Madsen, 19-Jun-2011.)
|
|
|
Theorem | disj1 3383* |
Two ways of saying that two classes are disjoint (have no members in
common). (Contributed by NM, 19-Aug-1993.)
|
|
|
Theorem | reldisj 3384 |
Two ways of saying that two classes are disjoint, using the complement
of relative to
a universe .
(Contributed by NM,
15-Feb-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | disj3 3385 |
Two ways of saying that two classes are disjoint. (Contributed by NM,
19-May-1998.)
|
|
|
Theorem | disjne 3386 |
Members of disjoint sets are not equal. (Contributed by NM,
28-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | disjel 3387 |
A set can't belong to both members of disjoint classes. (Contributed by
NM, 28-Feb-2015.)
|
|
|
Theorem | disj2 3388 |
Two ways of saying that two classes are disjoint. (Contributed by NM,
17-May-1998.)
|
|
|
Theorem | ssdisj 3389 |
Intersection with a subclass of a disjoint class. (Contributed by FL,
24-Jan-2007.)
|
|
|
Theorem | undisj1 3390 |
The union of disjoint classes is disjoint. (Contributed by NM,
26-Sep-2004.)
|
|
|
Theorem | undisj2 3391 |
The union of disjoint classes is disjoint. (Contributed by NM,
13-Sep-2004.)
|
|
|
Theorem | ssindif0im 3392 |
Subclass implies empty intersection with difference from the universal
class. (Contributed by NM, 17-Sep-2003.)
|
|
|
Theorem | inelcm 3393 |
The intersection of classes with a common member is nonempty.
(Contributed by NM, 7-Apr-1994.)
|
|
|
Theorem | minel 3394 |
A minimum element of a class has no elements in common with the class.
(Contributed by NM, 22-Jun-1994.)
|
|
|
Theorem | undif4 3395 |
Distribute union over difference. (Contributed by NM, 17-May-1998.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | disjssun 3396 |
Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | ssdif0im 3397 |
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, 2-Aug-2018.)
|
|
|
Theorem | vdif0im 3398 |
Universal class equality in terms of empty difference. (Contributed by
Jim Kingdon, 3-Aug-2018.)
|
|
|
Theorem | difrab0eqim 3399* |
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, 3-Aug-2018.)
|
|
|
Theorem | inssdif0im 3400 |
Intersection, subclass, and difference relationship. In classical logic
the converse would also hold. (Contributed by Jim Kingdon,
3-Aug-2018.)
|
|