Theorem List for Intuitionistic Logic Explorer - 3301-3400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ineq1 3301 |
Equality theorem for intersection of two classes. (Contributed by NM,
14-Dec-1993.)
|
|
|
Theorem | ineq2 3302 |
Equality theorem for intersection of two classes. (Contributed by NM,
26-Dec-1993.)
|
|
|
Theorem | ineq12 3303 |
Equality theorem for intersection of two classes. (Contributed by NM,
8-May-1994.)
|
|
|
Theorem | ineq1i 3304 |
Equality inference for intersection of two classes. (Contributed by NM,
26-Dec-1993.)
|
|
|
Theorem | ineq2i 3305 |
Equality inference for intersection of two classes. (Contributed by NM,
26-Dec-1993.)
|
|
|
Theorem | ineq12i 3306 |
Equality inference for intersection of two classes. (Contributed by
NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
|
|
|
Theorem | ineq1d 3307 |
Equality deduction for intersection of two classes. (Contributed by NM,
10-Apr-1994.)
|
|
|
Theorem | ineq2d 3308 |
Equality deduction for intersection of two classes. (Contributed by NM,
10-Apr-1994.)
|
|
|
Theorem | ineq12d 3309 |
Equality deduction for intersection of two classes. (Contributed by
NM, 24-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | ineqan12d 3310 |
Equality deduction for intersection of two classes. (Contributed by
NM, 7-Feb-2007.)
|
|
|
Theorem | dfss1 3311 |
A frequently-used variant of subclass definition df-ss 3115. (Contributed
by NM, 10-Jan-2015.)
|
|
|
Theorem | dfss5 3312 |
Another definition of subclasshood. Similar to df-ss 3115, dfss 3116, and
dfss1 3311. (Contributed by David Moews, 1-May-2017.)
|
|
|
Theorem | nfin 3313 |
Bound-variable hypothesis builder for the intersection of classes.
(Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro,
14-Oct-2016.)
|
|
|
Theorem | csbing 3314 |
Distribute proper substitution through an intersection relation.
(Contributed by Alan Sare, 22-Jul-2012.)
|
|
|
Theorem | rabbi2dva 3315* |
Deduction from a wff to a restricted class abstraction. (Contributed by
NM, 14-Jan-2014.)
|
|
|
Theorem | inidm 3316 |
Idempotent law for intersection of classes. Theorem 15 of [Suppes]
p. 26. (Contributed by NM, 5-Aug-1993.)
|
|
|
Theorem | inass 3317 |
Associative law for intersection of classes. Exercise 9 of
[TakeutiZaring] p. 17.
(Contributed by NM, 3-May-1994.)
|
|
|
Theorem | in12 3318 |
A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.)
|
|
|
Theorem | in32 3319 |
A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | in13 3320 |
A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
|
|
|
Theorem | in31 3321 |
A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
|
|
|
Theorem | inrot 3322 |
Rotate the intersection of 3 classes. (Contributed by NM,
27-Aug-2012.)
|
|
|
Theorem | in4 3323 |
Rearrangement of intersection of 4 classes. (Contributed by NM,
21-Apr-2001.)
|
|
|
Theorem | inindi 3324 |
Intersection distributes over itself. (Contributed by NM, 6-May-1994.)
|
|
|
Theorem | inindir 3325 |
Intersection distributes over itself. (Contributed by NM,
17-Aug-2004.)
|
|
|
Theorem | sseqin2 3326 |
A relationship between subclass and intersection. Similar to Exercise 9
of [TakeutiZaring] p. 18.
(Contributed by NM, 17-May-1994.)
|
|
|
Theorem | inss1 3327 |
The intersection of two classes is a subset of one of them. Part of
Exercise 12 of [TakeutiZaring] p.
18. (Contributed by NM,
27-Apr-1994.)
|
|
|
Theorem | inss2 3328 |
The intersection of two classes is a subset of one of them. Part of
Exercise 12 of [TakeutiZaring] p.
18. (Contributed by NM,
27-Apr-1994.)
|
|
|
Theorem | ssin 3329 |
Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26.
(Contributed by NM, 15-Jun-2004.) (Proof shortened by Andrew Salmon,
26-Jun-2011.)
|
|
|
Theorem | ssini 3330 |
An inference showing that a subclass of two classes is a subclass of
their intersection. (Contributed by NM, 24-Nov-2003.)
|
|
|
Theorem | ssind 3331 |
A deduction showing that a subclass of two classes is a subclass of
their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|
|
|
Theorem | ssrin 3332 |
Add right intersection to subclass relation. (Contributed by NM,
16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | sslin 3333 |
Add left intersection to subclass relation. (Contributed by NM,
19-Oct-1999.)
|
|
|
Theorem | ssrind 3334 |
Add right intersection to subclass relation. (Contributed by Glauco
Siliprandi, 2-Jan-2022.)
|
|
|
Theorem | ss2in 3335 |
Intersection of subclasses. (Contributed by NM, 5-May-2000.)
|
|
|
Theorem | ssinss1 3336 |
Intersection preserves subclass relationship. (Contributed by NM,
14-Sep-1999.)
|
|
|
Theorem | inss 3337 |
Inclusion of an intersection of two classes. (Contributed by NM,
30-Oct-2014.)
|
|
|
2.1.13.4 Combinations of difference, union, and
intersection of two classes
|
|
Theorem | unabs 3338 |
Absorption law for union. (Contributed by NM, 16-Apr-2006.)
|
|
|
Theorem | inabs 3339 |
Absorption law for intersection. (Contributed by NM, 16-Apr-2006.)
|
|
|
Theorem | dfss4st 3340* |
Subclass defined in terms of class difference. (Contributed by NM,
22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
STAB
|
|
Theorem | ssddif 3341 |
Double complement and subset. Similar to ddifss 3345 but inside a class
instead of the
universal class .
In classical logic the
subset operation on the right hand side could be an equality (that is,
).
(Contributed by Jim Kingdon,
24-Jul-2018.)
|
|
|
Theorem | unssdif 3342 |
Union of two classes and class difference. In classical logic this
would be an equality. (Contributed by Jim Kingdon, 24-Jul-2018.)
|
|
|
Theorem | inssdif 3343 |
Intersection of two classes and class difference. In classical logic
this would be an equality. (Contributed by Jim Kingdon,
24-Jul-2018.)
|
|
|
Theorem | difin 3344 |
Difference with intersection. Theorem 33 of [Suppes] p. 29.
(Contributed by NM, 31-Mar-1998.) (Proof shortened by Andrew Salmon,
26-Jun-2011.)
|
|
|
Theorem | ddifss 3345 |
Double complement under universal class. In classical logic (or given an
additional hypothesis, as in ddifnel 3238), this is equality rather than
subset. (Contributed by Jim Kingdon, 24-Jul-2018.)
|
|
|
Theorem | unssin 3346 |
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, 25-Jul-2018.)
|
|
|
Theorem | inssun 3347 |
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, 25-Jul-2018.)
|
|
|
Theorem | inssddif 3348 |
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, 26-Jul-2018.)
|
|
|
Theorem | invdif 3349 |
Intersection with universal complement. Remark in [Stoll] p. 20.
(Contributed by NM, 17-Aug-2004.)
|
|
|
Theorem | indif 3350 |
Intersection with class difference. Theorem 34 of [Suppes] p. 29.
(Contributed by NM, 17-Aug-2004.)
|
|
|
Theorem | indif2 3351 |
Bring an intersection in and out of a class difference. (Contributed by
Jeff Hankins, 15-Jul-2009.)
|
|
|
Theorem | indif1 3352 |
Bring an intersection in and out of a class difference. (Contributed by
Mario Carneiro, 15-May-2015.)
|
|
|
Theorem | indifcom 3353 |
Commutation law for intersection and difference. (Contributed by Scott
Fenton, 18-Feb-2013.)
|
|
|
Theorem | indi 3354 |
Distributive law for intersection over union. Exercise 10 of
[TakeutiZaring] p. 17.
(Contributed by NM, 30-Sep-2002.) (Proof
shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | undi 3355 |
Distributive law for union over intersection. Exercise 11 of
[TakeutiZaring] p. 17.
(Contributed by NM, 30-Sep-2002.) (Proof
shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | indir 3356 |
Distributive law for intersection over union. Theorem 28 of [Suppes]
p. 27. (Contributed by NM, 30-Sep-2002.)
|
|
|
Theorem | undir 3357 |
Distributive law for union over intersection. Theorem 29 of [Suppes]
p. 27. (Contributed by NM, 30-Sep-2002.)
|
|
|
Theorem | uneqin 3358 |
Equality of union and intersection implies equality of their arguments.
(Contributed by NM, 16-Apr-2006.) (Proof shortened by Andrew Salmon,
26-Jun-2011.)
|
|
|
Theorem | difundi 3359 |
Distributive law for class difference. Theorem 39 of [Suppes] p. 29.
(Contributed by NM, 17-Aug-2004.)
|
|
|
Theorem | difundir 3360 |
Distributive law for class difference. (Contributed by NM,
17-Aug-2004.)
|
|
|
Theorem | difindiss 3361 |
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, 26-Jul-2018.)
|
|
|
Theorem | difindir 3362 |
Distributive law for class difference. (Contributed by NM,
17-Aug-2004.)
|
|
|
Theorem | indifdir 3363 |
Distribute intersection over difference. (Contributed by Scott Fenton,
14-Apr-2011.)
|
|
|
Theorem | difdif2ss 3364 |
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 3365 |
De Morgan's law for union. Theorem 5.2(13) of [Stoll] p. 19.
(Contributed by NM, 18-Aug-2004.)
|
|
|
Theorem | indmss 3366 |
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 3367 |
A relationship involving double difference and union. (Contributed by NM,
29-Aug-2004.)
|
|
|
Theorem | undif3ss 3368 |
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 3369 |
Represent a set difference as an intersection with a larger difference.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | dif32 3370 |
Swap second and third argument of double difference. (Contributed by NM,
18-Aug-2004.)
|
|
|
Theorem | difabs 3371 |
Absorption-like law for class difference: you can remove a class only
once. (Contributed by FL, 2-Aug-2009.)
|
|
|
Theorem | symdif1 3372 |
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 3373* |
Expressing symmetric difference with exclusive-or or two differences.
(Contributed by Jim Kingdon, 28-Jul-2018.)
|
|
|
Theorem | unab 3374 |
Union of two class abstractions. (Contributed by NM, 29-Sep-2002.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | inab 3375 |
Intersection of two class abstractions. (Contributed by NM,
29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | difab 3376 |
Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | notab 3377 |
A class builder defined by a negation. (Contributed by FL,
18-Sep-2010.)
|
|
|
Theorem | unrab 3378 |
Union of two restricted class abstractions. (Contributed by NM,
25-Mar-2004.)
|
|
|
Theorem | inrab 3379 |
Intersection of two restricted class abstractions. (Contributed by NM,
1-Sep-2006.)
|
|
|
Theorem | inrab2 3380* |
Intersection with a restricted class abstraction. (Contributed by NM,
19-Nov-2007.)
|
|
|
Theorem | difrab 3381 |
Difference of two restricted class abstractions. (Contributed by NM,
23-Oct-2004.)
|
|
|
Theorem | dfrab2 3382* |
Alternate definition of restricted class abstraction. (Contributed by
NM, 20-Sep-2003.)
|
|
|
Theorem | dfrab3 3383* |
Alternate definition of restricted class abstraction. (Contributed by
Mario Carneiro, 8-Sep-2013.)
|
|
|
Theorem | notrab 3384* |
Complementation of restricted class abstractions. (Contributed by Mario
Carneiro, 3-Sep-2015.)
|
|
|
Theorem | dfrab3ss 3385* |
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 3386 |
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 3387* |
Transfer uniqueness to a smaller subclass. (Contributed by NM,
20-Oct-2005.)
|
|
|
Theorem | reuss 3388* |
Transfer uniqueness to a smaller subclass. (Contributed by NM,
21-Aug-1999.)
|
|
|
Theorem | reuun1 3389* |
Transfer uniqueness to a smaller class. (Contributed by NM,
21-Oct-2005.)
|
|
|
Theorem | reuun2 3390* |
Transfer uniqueness to a smaller or larger class. (Contributed by NM,
21-Oct-2005.)
|
|
|
Theorem | reupick 3391* |
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
NM, 21-Aug-1999.)
|
|
|
Theorem | reupick3 3392* |
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
Mario Carneiro, 19-Nov-2016.)
|
|
|
Theorem | reupick2 3393* |
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 3394 |
Extend class notation to include the empty set.
|
|
|
Definition | df-nul 3395 |
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 3396. (Contributed by NM, 5-Aug-1993.)
|
|
|
Theorem | dfnul2 3396 |
Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring]
p. 20. (Contributed by NM, 26-Dec-1996.)
|
|
|
Theorem | dfnul3 3397 |
Alternate definition of the empty set. (Contributed by NM,
25-Mar-2004.)
|
|
|
Theorem | noel 3398 |
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 3399 |
If a set has elements, it is not empty. A set with elements is also
inhabited, see elex2 2728. (Contributed by NM, 31-Dec-1993.)
|
|
|
Theorem | ne0i 3400 |
If a set has elements, it is not empty. A set with elements is also
inhabited, see elex2 2728. (Contributed by NM, 31-Dec-1993.)
|
|