Theorem List for Intuitionistic Logic Explorer - 3201-3300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | elinel1 3201 |
Membership in an intersection implies membership in the first set.
(Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
  
  |
|
Theorem | elinel2 3202 |
Membership in an intersection implies membership in the second set.
(Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
  
  |
|
Theorem | elin2 3203 |
Membership in a class defined as an intersection. (Contributed by
Stefan O'Rear, 29-Mar-2015.)
|
       |
|
Theorem | elin1d 3204 |
Elementhood in the first set of an intersection - deduction version.
(Contributed by Thierry Arnoux, 3-May-2020.)
|
       |
|
Theorem | elin2d 3205 |
Elementhood in the first set of an intersection - deduction version.
(Contributed by Thierry Arnoux, 3-May-2020.)
|
       |
|
Theorem | elin3 3206 |
Membership in a class defined as a ternary intersection. (Contributed
by Stefan O'Rear, 29-Mar-2015.)
|
     
   |
|
Theorem | incom 3207 |
Commutative law for intersection of classes. Exercise 7 of
[TakeutiZaring] p. 17.
(Contributed by NM, 5-Aug-1993.)
|
 
   |
|
Theorem | ineqri 3208* |
Inference from membership to intersection. (Contributed by NM,
5-Aug-1993.)
|
  
  
 |
|
Theorem | ineq1 3209 |
Equality theorem for intersection of two classes. (Contributed by NM,
14-Dec-1993.)
|
  
    |
|
Theorem | ineq2 3210 |
Equality theorem for intersection of two classes. (Contributed by NM,
26-Dec-1993.)
|
  
    |
|
Theorem | ineq12 3211 |
Equality theorem for intersection of two classes. (Contributed by NM,
8-May-1994.)
|
         |
|
Theorem | ineq1i 3212 |
Equality inference for intersection of two classes. (Contributed by NM,
26-Dec-1993.)
|
     |
|
Theorem | ineq2i 3213 |
Equality inference for intersection of two classes. (Contributed by NM,
26-Dec-1993.)
|
     |
|
Theorem | ineq12i 3214 |
Equality inference for intersection of two classes. (Contributed by
NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
|
 
   |
|
Theorem | ineq1d 3215 |
Equality deduction for intersection of two classes. (Contributed by NM,
10-Apr-1994.)
|
         |
|
Theorem | ineq2d 3216 |
Equality deduction for intersection of two classes. (Contributed by NM,
10-Apr-1994.)
|
         |
|
Theorem | ineq12d 3217 |
Equality deduction for intersection of two classes. (Contributed by
NM, 24-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
           |
|
Theorem | ineqan12d 3218 |
Equality deduction for intersection of two classes. (Contributed by
NM, 7-Feb-2007.)
|
             |
|
Theorem | dfss1 3219 |
A frequently-used variant of subclass definition df-ss 3026. (Contributed
by NM, 10-Jan-2015.)
|
     |
|
Theorem | dfss5 3220 |
Another definition of subclasshood. Similar to df-ss 3026, dfss 3027, and
dfss1 3219. (Contributed by David Moews, 1-May-2017.)
|
     |
|
Theorem | nfin 3221 |
Bound-variable hypothesis builder for the intersection of classes.
(Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro,
14-Oct-2016.)
|
         |
|
Theorem | csbing 3222 |
Distribute proper substitution through an intersection relation.
(Contributed by Alan Sare, 22-Jul-2012.)
|
   ![]_ ]_](_urbrack.gif)  
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
|
Theorem | rabbi2dva 3223* |
Deduction from a wff to a restricted class abstraction. (Contributed by
NM, 14-Jan-2014.)
|
   
         |
|
Theorem | inidm 3224 |
Idempotent law for intersection of classes. Theorem 15 of [Suppes]
p. 26. (Contributed by NM, 5-Aug-1993.)
|
 
 |
|
Theorem | inass 3225 |
Associative law for intersection of classes. Exercise 9 of
[TakeutiZaring] p. 17.
(Contributed by NM, 3-May-1994.)
|
     
   |
|
Theorem | in12 3226 |
A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.)
|
     
   |
|
Theorem | in32 3227 |
A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
         |
|
Theorem | in13 3228 |
A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
|
     
   |
|
Theorem | in31 3229 |
A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
|
         |
|
Theorem | inrot 3230 |
Rotate the intersection of 3 classes. (Contributed by NM,
27-Aug-2012.)
|
         |
|
Theorem | in4 3231 |
Rearrangement of intersection of 4 classes. (Contributed by NM,
21-Apr-2001.)
|
             |
|
Theorem | inindi 3232 |
Intersection distributes over itself. (Contributed by NM, 6-May-1994.)
|
           |
|
Theorem | inindir 3233 |
Intersection distributes over itself. (Contributed by NM,
17-Aug-2004.)
|
           |
|
Theorem | sseqin2 3234 |
A relationship between subclass and intersection. Similar to Exercise 9
of [TakeutiZaring] p. 18.
(Contributed by NM, 17-May-1994.)
|
     |
|
Theorem | inss1 3235 |
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 3236 |
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 3237 |
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 3238 |
An inference showing that a subclass of two classes is a subclass of
their intersection. (Contributed by NM, 24-Nov-2003.)
|
   |
|
Theorem | ssind 3239 |
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 3240 |
Add right intersection to subclass relation. (Contributed by NM,
16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
       |
|
Theorem | sslin 3241 |
Add left intersection to subclass relation. (Contributed by NM,
19-Oct-1999.)
|
       |
|
Theorem | ssrind 3242 |
Add right intersection to subclass relation. (Contributed by Glauco
Siliprandi, 2-Jan-2022.)
|
     
   |
|
Theorem | ss2in 3243 |
Intersection of subclasses. (Contributed by NM, 5-May-2000.)
|
    
    |
|
Theorem | ssinss1 3244 |
Intersection preserves subclass relationship. (Contributed by NM,
14-Sep-1999.)
|
     |
|
Theorem | inss 3245 |
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 3246 |
Absorption law for union. (Contributed by NM, 16-Apr-2006.)
|
     |
|
Theorem | inabs 3247 |
Absorption law for intersection. (Contributed by NM, 16-Apr-2006.)
|
     |
|
Theorem | dfss4st 3248* |
Subclass defined in terms of class difference. (Contributed by NM,
22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
  STAB
  
     |
|
Theorem | ssddif 3249 |
Double complement and subset. Similar to ddifss 3253 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 3250 |
Union of two classes and class difference. In classical logic this
would be an equality. (Contributed by Jim Kingdon, 24-Jul-2018.)
|
         |
|
Theorem | inssdif 3251 |
Intersection of two classes and class difference. In classical logic
this would be an equality. (Contributed by Jim Kingdon,
24-Jul-2018.)
|
       |
|
Theorem | difin 3252 |
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 3253 |
Double complement under universal class. In classical logic (or given an
additional hypothesis, as in ddifnel 3146), this is equality rather than
subset. (Contributed by Jim Kingdon, 24-Jul-2018.)
|
     |
|
Theorem | unssin 3254 |
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 3255 |
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 3256 |
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 3257 |
Intersection with universal complement. Remark in [Stoll] p. 20.
(Contributed by NM, 17-Aug-2004.)
|
       |
|
Theorem | indif 3258 |
Intersection with class difference. Theorem 34 of [Suppes] p. 29.
(Contributed by NM, 17-Aug-2004.)
|
       |
|
Theorem | indif2 3259 |
Bring an intersection in and out of a class difference. (Contributed by
Jeff Hankins, 15-Jul-2009.)
|
         |
|
Theorem | indif1 3260 |
Bring an intersection in and out of a class difference. (Contributed by
Mario Carneiro, 15-May-2015.)
|
  
      |
|
Theorem | indifcom 3261 |
Commutation law for intersection and difference. (Contributed by Scott
Fenton, 18-Feb-2013.)
|
     
   |
|
Theorem | indi 3262 |
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 3263 |
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 3264 |
Distributive law for intersection over union. Theorem 28 of [Suppes]
p. 27. (Contributed by NM, 30-Sep-2002.)
|
  
        |
|
Theorem | undir 3265 |
Distributive law for union over intersection. Theorem 29 of [Suppes]
p. 27. (Contributed by NM, 30-Sep-2002.)
|
           |
|
Theorem | uneqin 3266 |
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 3267 |
Distributive law for class difference. Theorem 39 of [Suppes] p. 29.
(Contributed by NM, 17-Aug-2004.)
|
           |
|
Theorem | difundir 3268 |
Distributive law for class difference. (Contributed by NM,
17-Aug-2004.)
|
  
        |
|
Theorem | difindiss 3269 |
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 3270 |
Distributive law for class difference. (Contributed by NM,
17-Aug-2004.)
|
           |
|
Theorem | indifdir 3271 |
Distribute intersection over difference. (Contributed by Scott Fenton,
14-Apr-2011.)
|
  
    
   |
|
Theorem | difdif2ss 3272 |
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 3273 |
De Morgan's law for union. Theorem 5.2(13) of [Stoll] p. 19.
(Contributed by NM, 18-Aug-2004.)
|
           |
|
Theorem | indmss 3274 |
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 3275 |
A relationship involving double difference and union. (Contributed by NM,
29-Aug-2004.)
|
         |
|
Theorem | undif3ss 3276 |
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 3277 |
Represent a set difference as an intersection with a larger difference.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
  
      |
|
Theorem | dif32 3278 |
Swap second and third argument of double difference. (Contributed by NM,
18-Aug-2004.)
|
  
      |
|
Theorem | difabs 3279 |
Absorption-like law for class difference: you can remove a class only
once. (Contributed by FL, 2-Aug-2009.)
|
  
    |
|
Theorem | symdif1 3280 |
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 3281* |
Expressing symmetric difference with exclusive-or or two differences.
(Contributed by Jim Kingdon, 28-Jul-2018.)
|
  
    
   |
|
Theorem | unab 3282 |
Union of two class abstractions. (Contributed by NM, 29-Sep-2002.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
       
   |
|
Theorem | inab 3283 |
Intersection of two class abstractions. (Contributed by NM,
29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
  
    
   |
|
Theorem | difab 3284 |
Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.)
(Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
  
    
   |
|
Theorem | notab 3285 |
A class builder defined by a negation. (Contributed by FL,
18-Sep-2010.)
|
       |
|
Theorem | unrab 3286 |
Union of two restricted class abstractions. (Contributed by NM,
25-Mar-2004.)
|
      
    |
|
Theorem | inrab 3287 |
Intersection of two restricted class abstractions. (Contributed by NM,
1-Sep-2006.)
|
      
    |
|
Theorem | inrab2 3288* |
Intersection with a restricted class abstraction. (Contributed by NM,
19-Nov-2007.)
|
      
  |
|
Theorem | difrab 3289 |
Difference of two restricted class abstractions. (Contributed by NM,
23-Oct-2004.)
|
   
       |
|
Theorem | dfrab2 3290* |
Alternate definition of restricted class abstraction. (Contributed by
NM, 20-Sep-2003.)
|
       |
|
Theorem | dfrab3 3291* |
Alternate definition of restricted class abstraction. (Contributed by
Mario Carneiro, 8-Sep-2013.)
|
       |
|
Theorem | notrab 3292* |
Complementation of restricted class abstractions. (Contributed by Mario
Carneiro, 3-Sep-2015.)
|
 
  
  |
|
Theorem | dfrab3ss 3293* |
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 3294 |
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 3295* |
Transfer uniqueness to a smaller subclass. (Contributed by NM,
20-Oct-2005.)
|
   
        
  |
|
Theorem | reuss 3296* |
Transfer uniqueness to a smaller subclass. (Contributed by NM,
21-Aug-1999.)
|
  
  
  |
|
Theorem | reuun1 3297* |
Transfer uniqueness to a smaller class. (Contributed by NM,
21-Oct-2005.)
|
  
       
  |
|
Theorem | reuun2 3298* |
Transfer uniqueness to a smaller or larger class. (Contributed by NM,
21-Oct-2005.)
|
 
     
   |
|
Theorem | reupick 3299* |
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
NM, 21-Aug-1999.)
|
    
        |
|
Theorem | reupick3 3300* |
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
Mario Carneiro, 19-Nov-2016.)
|
  
        |