Statement List for Metamath Proof Explorer - 2101-2200 - Page 22 of 107
| Type | Label | Description |
| Statement |
| |
| Theorem | syl5ss 2101 |
A chained subclass and equality deduction.
|
     |
| |
| Theorem | syl5ssr 2102 |
A chained subclass and equality deduction.
|
     |
| |
| Theorem | syl6ss 2103 |
A chained subclass and equality deduction.
|
     |
| |
| Theorem | syl6ssr 2104 |
A chained subclass and equality deduction.
|
     |
| |
| Theorem | eqimss 2105 |
Equality implies the subclass relation.
|
   |
| |
| Theorem | eqimss2 2106 |
Equality implies the subclass relation.
|
   |
| |
| Theorem | eqimssi 2107 |
Infer subclass relationship from equality.
|
 |
| |
| Theorem | eqimss2i 2108 |
Infer subclass relationship from equality.
|
 |
| |
| Theorem | nss 2109 |
Negation of subclass relationship. Exercise 13 of [TakeutiZaring]
p. 18.
|
   
   |
| |
| Theorem | ssralv 2110 |
Quantification restricted to a subclass.
|
   
   |
| |
| Theorem | ssrexv 2111 |
Existential quantification restricted to a subclass.
|
   
   |
| |
| Theorem | ss2ab 2112 |
Class abstractions in a subclass relationship.
|
  
        |
| |
| Theorem | abss 2113 |
Class abstraction in a subclass relationship.
|
  
      |
| |
| Theorem | ssab 2114 |
Subclass of a class abstraction.
|
         |
| |
| Theorem | ssabral 2115 |
The relation for a subclass of a class abstraction is equivalent to
restricted quantification.
|
   
  |
| |
| Theorem | ss2abi 2116 |
Inference of abstraction subclass from implication.
|
       |
| |
| Theorem | abssdv 2117 |
Deduction of abstraction subclass from implication.
|
     
   |
| |
| Theorem | abssi 2118 |
Inference of abstraction subclass from implication.
|
     |
| |
| Theorem | ss2rab 2119 |
Restricted abstraction classes in a subclass relationship.
|
     
    |
| |
| Theorem | rabss 2120 |
Restricted class abstraction in a subclass relationship.
|
    
   |
| |
| Theorem | ssrab 2121 |
Subclass of a restricted class abstraction.
|
 
 
    |
| |
| Theorem | ssrabdv 2122 |
Subclass of a restricted class abstraction (deduction rule).
|
   

  
   |
| |
| Theorem | ss2rabdv 2123 |
Deduction of restricted abstraction subclass from implication.
|
 
     


   |
| |
| Theorem | ss2rabi 2124 |
Inference of restricted abstraction subclass from implication.
|
      
  |
| |
| Theorem | rabss2 2125 |
Subclass law for restricted abstraction.
|
   
   |
| |
| Theorem | ssab2 2126 |
Subclass relation for the restriction of a class abstraction.
|
     |
| |
| Theorem | ssrab2 2127 |
Subclass relation for a restricted class.
|
   |
| |
| Theorem | uniiunlem 2128 |
A subset relationship useful for converting union to indexed union using
dfiun2 2583 or dfiun2g 2582 and intersection to indexed intersection
using
dfiin2 2584.
|
     
    |
| |
| Theorem | dfpss2 2129 |
Alternate definition of proper subclass.
|
 
   |
| |
| Theorem | dfpss3 2130 |
Alternate definition of proper subclass.
|
 
   |
| |
| Theorem | psseq1 2131 |
Equality theorem for proper subclass.
|
     |
| |
| Theorem | psseq2 2132 |
Equality theorem for proper subclass.
|
     |
| |
| Theorem | psseq1i 2133 |
An equality inference for the proper subclass relationship.
|
   |
| |
| Theorem | psseq2i 2134 |
An equality inference for the proper subclass relationship.
|
   |
| |
| Theorem | psseq12i 2135 |
An equality inference for the proper subclass relationship.
|
   |
| |
| Theorem | psseq1d 2136 |
An equality deduction for the proper subclass relationship.
|
       |
| |
| Theorem | psseq2d 2137 |
An equality deduction for the proper subclass relationship.
|
       |
| |
| Theorem | psseq12d 2138 |
An equality deduction for the proper subclass relationship.
|
     
   |
| |
| Theorem | pssss 2139 |
A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23.
|
   |
| |
| Theorem | pssssd 2140 |
Deduce subclass from proper subclass.
|
     |
| |
| Theorem | sspss 2141 |
Subclass in terms of proper subclass.
|
 
   |
| |
| Theorem | pssirr 2142 |
Proper subclass is irreflexive. Theorem 7 of [Suppes] p. 23.
|
 |
| |
| Theorem | pssn2lp 2143 |
Proper subclass has no 2-cycle loops. Compare Theorem 8 of [Suppes]
p. 23.
|

  |
| |
| Theorem | sspsstri 2144 |
Two ways of stating trichotomy with respect to inclusion.
|
 
 
   |
| |
| Theorem | ssnpss 2145 |
Partial trichotomy law for subclasses.
|
   |
| |
| Theorem | psstr 2146 |
Transitive law for proper subclass. Theorem 9 of [Suppes] p. 23.
|
 
   |
| |
| Theorem | sspsstr 2147 |
Transitive law for subclass and proper subclass.
|
 
   |
| |
| Theorem | psssstr 2148 |
Transitive law for subclass and proper subclass.
|
 

  |
| |
| The
difference, union, and intersection of two classes |
| |
| Theorem | difeq1 2149 |
Equality theorem for class difference.
|
       |
| |
| Theorem | difeq2 2150 |
Equality theorem for class difference.
|
       |
| |
| Theorem | difeq1i 2151 |
Inference adding difference to the right in a class equality.
|
     |
| |
| Theorem | difeq2i 2152 |
Inference adding difference to the left in a class equality.
|
     |
| |
| Theorem | difeq12i 2153 |
Equality inference for class difference.
|
 
   |
| |
| Theorem | difeq1d 2154 |
Deduction adding difference to the right in a class equality.
|
         |
| |
| Theorem | difeq2d 2155 |
Deduction adding difference to the left in a class equality.
|
         |
| |
| Theorem | difeqri 2156 |
Inference from membership to difference.
|
     
 |
| |
| Theorem | hbdif 2157 |
Bound-variable hypothesis builder for class difference.
|
    
 
       |
| |
| Theorem | eldifi 2158 |
Implication of membership in a class difference.
|
     |
| |
| Theorem | eldifn 2159 |
Implication of membership in a class difference.
|
     |
| |
| Theorem | elndif 2160 |
A set does not belong to a class excluding it.
|
     |
| |
| Theorem | neldif 2161 |
Implication of membership in a class difference.
|
       |
| |
| Theorem | difdif 2162 |
Double class difference. Exercise 11 of [TakeutiZaring] p. 22.
|
     |
| |
| Theorem | difss 2163 |
Subclass relationship for class difference. Exercise 14 of
[TakeutiZaring] p. 22.
|
   |
| |
| Theorem | ssdifss 2164 |
Preservation of a subclass relationship by class difference.
|
     |
| |
| Theorem | ddif 2165 |
Double complement under universal class. Exercise 4.10(s) of
[Mendelson] p. 231.
|
     |
| |
| Theorem | ssconb 2166 |
Contraposition law for subsets.
|
 

        |
| |
| Theorem | sscon 2167 |
Contraposition law for subsets. Exercise 15 of [TakeutiZaring]
p. 22.
|
       |
| |
| Theorem | ssdif 2168 |
Difference law for subsets.
|
       |
| |
| Theorem | elun 2169 |
Expansion of membership in class union. Theorem 12 of [Suppes]
p. 25.
|
   
   |
| |
| Theorem | uneqri 2170 |
Inference from membership to union.
|
     
 |
| |
| Theorem | unidm 2171 |
Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27.
|
 
 |
| |
| Theorem | uncom 2172 |
Commutative law for union of classes. Exercise 6 of [TakeutiZaring]
p. 17.
|
 
   |
| |
| Theorem | uneq1 2173 |
Equality theorem for union of two classes.
|
       |
| |
| Theorem | uneq2 2174 |
Equality theorem for the union of two classes.
|
       |
| |
| Theorem | uneq12 2175 |
Equality theorem for union of two classes.
|
   
     |
| |
| Theorem | uneq1i 2176 |
Inference adding union to the right in a class equality.
|
   |