Theorem List for Intuitionistic Logic Explorer - 3301-3400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | inss1 3301 |
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.)
|
![( (](lp.gif) ![B B](_cb.gif) ![A A](_ca.gif) |
|
Theorem | inss2 3302 |
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.)
|
![( (](lp.gif) ![B B](_cb.gif) ![B B](_cb.gif) |
|
Theorem | ssin 3303 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ssini 3304 |
An inference showing that a subclass of two classes is a subclass of
their intersection. (Contributed by NM, 24-Nov-2003.)
|
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ssind 3305 |
A deduction showing that a subclass of two classes is a subclass of
their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ssrin 3306 |
Add right intersection to subclass relation. (Contributed by NM,
16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sslin 3307 |
Add left intersection to subclass relation. (Contributed by NM,
19-Oct-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ssrind 3308 |
Add right intersection to subclass relation. (Contributed by Glauco
Siliprandi, 2-Jan-2022.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ss2in 3309 |
Intersection of subclasses. (Contributed by NM, 5-May-2000.)
|
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ssinss1 3310 |
Intersection preserves subclass relationship. (Contributed by NM,
14-Sep-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | inss 3311 |
Inclusion of an intersection of two classes. (Contributed by NM,
30-Oct-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
2.1.13.4 Combinations of difference, union, and
intersection of two classes
|
|
Theorem | unabs 3312 |
Absorption law for union. (Contributed by NM, 16-Apr-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![A A](_ca.gif) |
|
Theorem | inabs 3313 |
Absorption law for intersection. (Contributed by NM, 16-Apr-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![A A](_ca.gif) |
|
Theorem | dfss4st 3314* |
Subclass defined in terms of class difference. (Contributed by NM,
22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
![( (](lp.gif) ![A. A.](forall.gif) STAB
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ssddif 3315 |
Double complement and subset. Similar to ddifss 3319 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,
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ).
(Contributed by Jim Kingdon,
24-Jul-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | unssdif 3316 |
Union of two classes and class difference. In classical logic this
would be an equality. (Contributed by Jim Kingdon, 24-Jul-2018.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | inssdif 3317 |
Intersection of two classes and class difference. In classical logic
this would be an equality. (Contributed by Jim Kingdon,
24-Jul-2018.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | difin 3318 |
Difference with intersection. Theorem 33 of [Suppes] p. 29.
(Contributed by NM, 31-Mar-1998.) (Proof shortened by Andrew Salmon,
26-Jun-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ddifss 3319 |
Double complement under universal class. In classical logic (or given an
additional hypothesis, as in ddifnel 3212), this is equality rather than
subset. (Contributed by Jim Kingdon, 24-Jul-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | unssin 3320 |
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.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | inssun 3321 |
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.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | inssddif 3322 |
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.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | invdif 3323 |
Intersection with universal complement. Remark in [Stoll] p. 20.
(Contributed by NM, 17-Aug-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | indif 3324 |
Intersection with class difference. Theorem 34 of [Suppes] p. 29.
(Contributed by NM, 17-Aug-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | indif2 3325 |
Bring an intersection in and out of a class difference. (Contributed by
Jeff Hankins, 15-Jul-2009.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | indif1 3326 |
Bring an intersection in and out of a class difference. (Contributed by
Mario Carneiro, 15-May-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | indifcom 3327 |
Commutation law for intersection and difference. (Contributed by Scott
Fenton, 18-Feb-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | indi 3328 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | undi 3329 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | indir 3330 |
Distributive law for intersection over union. Theorem 28 of [Suppes]
p. 27. (Contributed by NM, 30-Sep-2002.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | undir 3331 |
Distributive law for union over intersection. Theorem 29 of [Suppes]
p. 27. (Contributed by NM, 30-Sep-2002.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | uneqin 3332 |
Equality of union and intersection implies equality of their arguments.
(Contributed by NM, 16-Apr-2006.) (Proof shortened by Andrew Salmon,
26-Jun-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | difundi 3333 |
Distributive law for class difference. Theorem 39 of [Suppes] p. 29.
(Contributed by NM, 17-Aug-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | difundir 3334 |
Distributive law for class difference. (Contributed by NM,
17-Aug-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | difindiss 3335 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | difindir 3336 |
Distributive law for class difference. (Contributed by NM,
17-Aug-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | indifdir 3337 |
Distribute intersection over difference. (Contributed by Scott Fenton,
14-Apr-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | difdif2ss 3338 |
Set difference with a set difference. In classical logic this would be
equality rather than subset. (Contributed by Jim Kingdon,
27-Jul-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | undm 3339 |
De Morgan's law for union. Theorem 5.2(13) of [Stoll] p. 19.
(Contributed by NM, 18-Aug-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | indmss 3340 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | difun1 3341 |
A relationship involving double difference and union. (Contributed by NM,
29-Aug-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | undif3ss 3342 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | difin2 3343 |
Represent a set difference as an intersection with a larger difference.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![A
A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | dif32 3344 |
Swap second and third argument of double difference. (Contributed by NM,
18-Aug-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | difabs 3345 |
Absorption-like law for class difference: you can remove a class only
once. (Contributed by FL, 2-Aug-2009.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | symdif1 3346 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
2.1.13.5 Class abstractions with difference,
union, and intersection of two classes
|
|
Theorem | symdifxor 3347* |
Expressing symmetric difference with exclusive-or or two differences.
(Contributed by Jim Kingdon, 28-Jul-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | unab 3348 |
Union of two class abstractions. (Contributed by NM, 29-Sep-2002.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif) ![ps ps](_psi.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | inab 3349 |
Intersection of two class abstractions. (Contributed by NM,
29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif)
![{ {](lbrace.gif) ![ps ps](_psi.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | difab 3350 |
Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif)
![{ {](lbrace.gif) ![ps ps](_psi.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | notab 3351 |
A class builder defined by a negation. (Contributed by FL,
18-Sep-2010.)
|
![{
{](lbrace.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | unrab 3352 |
Union of two restricted class abstractions. (Contributed by NM,
25-Mar-2004.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif) ![ps ps](_psi.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif)
![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | inrab 3353 |
Intersection of two restricted class abstractions. (Contributed by NM,
1-Sep-2006.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif) ![ps ps](_psi.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif)
![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | inrab2 3354* |
Intersection with a restricted class abstraction. (Contributed by NM,
19-Nov-2007.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![B B](_cb.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![B B](_cb.gif)
![ph ph](_varphi.gif) ![} }](rbrace.gif) |
|
Theorem | difrab 3355 |
Difference of two restricted class abstractions. (Contributed by NM,
23-Oct-2004.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif)
![ps ps](_psi.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | dfrab2 3356* |
Alternate definition of restricted class abstraction. (Contributed by
NM, 20-Sep-2003.)
|
![{
{](lbrace.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | dfrab3 3357* |
Alternate definition of restricted class abstraction. (Contributed by
Mario Carneiro, 8-Sep-2013.)
|
![{
{](lbrace.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | notrab 3358* |
Complementation of restricted class abstractions. (Contributed by Mario
Carneiro, 3-Sep-2015.)
|
![( (](lp.gif) ![{ {](lbrace.gif)
![ph ph](_varphi.gif) ![}
}](rbrace.gif) ![{ {](lbrace.gif)
![ph ph](_varphi.gif) ![} }](rbrace.gif) |
|
Theorem | dfrab3ss 3359* |
Restricted class abstraction with a common superset. (Contributed by
Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro,
8-Nov-2015.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | rabun2 3360 |
Abstraction restricted to a union. (Contributed by Stefan O'Rear,
5-Feb-2015.)
|
![{
{](lbrace.gif) ![( (](lp.gif) ![B B](_cb.gif) ![ph
ph](_varphi.gif)
![( (](lp.gif) ![{ {](lbrace.gif)
![ph ph](_varphi.gif) ![{ {](lbrace.gif)
![ph ph](_varphi.gif) ![}
}](rbrace.gif) ![) )](rp.gif) |
|
2.1.13.6 Restricted uniqueness with difference,
union, and intersection
|
|
Theorem | reuss2 3361* |
Transfer uniqueness to a smaller subclass. (Contributed by NM,
20-Oct-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![E! E!](_e1.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![E! E!](_e1.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | reuss 3362* |
Transfer uniqueness to a smaller subclass. (Contributed by NM,
21-Aug-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![E! E!](_e1.gif) ![ph ph](_varphi.gif) ![E! E!](_e1.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | reuun1 3363* |
Transfer uniqueness to a smaller class. (Contributed by NM,
21-Oct-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![E! E!](_e1.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![E! E!](_e1.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | reuun2 3364* |
Transfer uniqueness to a smaller or larger class. (Contributed by NM,
21-Oct-2005.)
|
![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![E! E!](_e1.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![E! E!](_e1.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | reupick 3365* |
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
NM, 21-Aug-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![E! E!](_e1.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | reupick3 3366* |
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
Mario Carneiro, 19-Nov-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![E! E!](_e1.gif)
![E. E.](exists.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![A A](_ca.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | reupick2 3367* |
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
Mario Carneiro, 15-Dec-2013.) (Proof shortened by Mario Carneiro,
19-Nov-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![ph ph](_varphi.gif) ![E. E.](exists.gif)
![E!
E!](_e1.gif) ![ph ph](_varphi.gif) ![A A](_ca.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
2.1.14 The empty set
|
|
Syntax | c0 3368 |
Extend class notation to include the empty set.
|
![(/) (/)](varnothing.gif) |
|
Definition | df-nul 3369 |
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 3370. (Contributed by NM, 5-Aug-1993.)
|
![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | dfnul2 3370 |
Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring]
p. 20. (Contributed by NM, 26-Dec-1996.)
|
![{ {](lbrace.gif)
![x x](_x.gif) ![} }](rbrace.gif) |
|
Theorem | dfnul3 3371 |
Alternate definition of the empty set. (Contributed by NM,
25-Mar-2004.)
|
![{ {](lbrace.gif) ![A A](_ca.gif) ![} }](rbrace.gif) |
|
Theorem | noel 3372 |
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.)
|
![(/) (/)](varnothing.gif) |
|
Theorem | n0i 3373 |
If a set has elements, it is not empty. A set with elements is also
inhabited, see elex2 2705. (Contributed by NM, 31-Dec-1993.)
|
![( (](lp.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | ne0i 3374 |
If a set has elements, it is not empty. A set with elements is also
inhabited, see elex2 2705. (Contributed by NM, 31-Dec-1993.)
|
![( (](lp.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | ne0d 3375 |
Deduction form of ne0i 3374. If a class has elements, then it is
nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![(/)
(/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | n0ii 3376 |
If a class has elements, then it is not empty. Inference associated
with n0i 3373. (Contributed by BJ, 15-Jul-2021.)
|
![(/) (/)](varnothing.gif) |
|
Theorem | ne0ii 3377 |
If a class has elements, then it is nonempty. Inference associated with
ne0i 3374. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
![(/) (/)](varnothing.gif) |
|
Theorem | vn0 3378 |
The universal class is not equal to the empty set. (Contributed by NM,
11-Sep-2008.)
|
![(/) (/)](varnothing.gif) |
|
Theorem | vn0m 3379 |
The universal class is inhabited. (Contributed by Jim Kingdon,
17-Dec-2018.)
|
![E.
E.](exists.gif) ![_V
_V](rmcv.gif) |
|
Theorem | n0rf 3380 |
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 3381 requires only that not be free in,
rather than not occur in, . (Contributed by Jim Kingdon,
31-Jul-2018.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![(/)
(/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | n0r 3381* |
An inhabited class is nonempty. See n0rf 3380 for more discussion.
(Contributed by Jim Kingdon, 31-Jul-2018.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![(/)
(/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | neq0r 3382* |
An inhabited class is nonempty. See n0rf 3380 for more discussion.
(Contributed by Jim Kingdon, 31-Jul-2018.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | reximdva0m 3383* |
Restricted existence deduced from inhabited class. (Contributed by Jim
Kingdon, 31-Jul-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![(
(](lp.gif)
![E. E.](exists.gif)
![A A](_ca.gif) ![E. E.](exists.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
|
Theorem | n0mmoeu 3384* |
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.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![E* E*](_em1.gif)
![E! E!](_e1.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | rex0 3385 |
Vacuous existential quantification is false. (Contributed by NM,
15-Oct-2003.)
|
![E. E.](exists.gif) ![ph ph](_varphi.gif) |
|
Theorem | eq0 3386* |
The empty set has no elements. Theorem 2 of [Suppes] p. 22.
(Contributed by NM, 29-Aug-1993.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | eqv 3387* |
The universe contains every set. (Contributed by NM, 11-Sep-2006.)
|
![( (](lp.gif) ![A. A.](forall.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | notm0 3388* |
A class is not inhabited if and only if it is empty. (Contributed by
Jim Kingdon, 1-Jul-2022.)
|
![( (](lp.gif) ![E. E.](exists.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | nel0 3389* |
From the general negation of membership in , infer that is
the empty set. (Contributed by BJ, 6-Oct-2018.)
|
![(/) (/)](varnothing.gif) |
|
Theorem | 0el 3390* |
Membership of the empty set in another class. (Contributed by NM,
29-Jun-2004.)
|
![( (](lp.gif)
![E. E.](exists.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![) )](rp.gif) |
|
Theorem | abvor0dc 3391* |
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 ![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | abn0r 3392 |
Nonempty class abstraction. (Contributed by Jim Kingdon, 1-Aug-2018.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | abn0m 3393* |
Inhabited class abstraction. (Contributed by Jim Kingdon,
8-Jul-2022.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![E.
E.](exists.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | rabn0r 3394 |
Nonempty restricted class abstraction. (Contributed by Jim Kingdon,
1-Aug-2018.)
|
![( (](lp.gif) ![E. E.](exists.gif)
![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | rabn0m 3395* |
Inhabited restricted class abstraction. (Contributed by Jim Kingdon,
18-Sep-2018.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![E. E.](exists.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | rab0 3396 |
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.)
|
![{
{](lbrace.gif) ![ph ph](_varphi.gif) ![(/) (/)](varnothing.gif) |
|
Theorem | rabeq0 3397 |
Condition for a restricted class abstraction to be empty. (Contributed
by Jeff Madsen, 7-Jun-2010.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![A. A.](forall.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | abeq0 3398 |
Condition for a class abstraction to be empty. (Contributed by Jim
Kingdon, 12-Aug-2018.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![A. A.](forall.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | rabxmdc 3399* |
Law of excluded middle given decidability, in terms of restricted class
abstractions. (Contributed by Jim Kingdon, 2-Aug-2018.)
|
![( (](lp.gif) ![A. A.](forall.gif) DECID ![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | rabnc 3400* |
Law of noncontradiction, in terms of restricted class abstractions.
(Contributed by Jeff Madsen, 20-Jun-2011.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![} }](rbrace.gif) ![(/) (/)](varnothing.gif) |