Theorem List for Intuitionistic Logic Explorer - 2101-2200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | eqidd 2101 |
Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)
|
   |
|
Theorem | eqcom 2102 |
Commutative law for class equality. Theorem 6.5 of [Quine] p. 41.
(Contributed by NM, 5-Aug-1993.)
|
   |
|
Theorem | eqcoms 2103 |
Inference applying commutative law for class equality to an antecedent.
(Contributed by NM, 5-Aug-1993.)
|
     |
|
Theorem | eqcomi 2104 |
Inference from commutative law for class equality. (Contributed by NM,
5-Aug-1993.)
|
 |
|
Theorem | eqcomd 2105 |
Deduction from commutative law for class equality. (Contributed by NM,
15-Aug-1994.)
|
     |
|
Theorem | eqeq1 2106 |
Equality implies equivalence of equalities. (Contributed by NM,
5-Aug-1993.)
|
     |
|
Theorem | eqeq1i 2107 |
Inference from equality to equivalence of equalities. (Contributed by
NM, 5-Aug-1993.)
|
   |
|
Theorem | eqeq1d 2108 |
Deduction from equality to equivalence of equalities. (Contributed by
NM, 27-Dec-1993.)
|
   
   |
|
Theorem | eqeq2 2109 |
Equality implies equivalence of equalities. (Contributed by NM,
5-Aug-1993.)
|
     |
|
Theorem | eqeq2i 2110 |
Inference from equality to equivalence of equalities. (Contributed by
NM, 5-Aug-1993.)
|
   |
|
Theorem | eqeq2d 2111 |
Deduction from equality to equivalence of equalities. (Contributed by
NM, 27-Dec-1993.)
|
   
   |
|
Theorem | eqeq12 2112 |
Equality relationship among 4 classes. (Contributed by NM,
3-Aug-1994.)
|
       |
|
Theorem | eqeq12i 2113 |
A useful inference for substituting definitions into an equality.
(Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon,
25-May-2011.)
|
   |
|
Theorem | eqeq12d 2114 |
A useful inference for substituting definitions into an equality.
(Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon,
25-May-2011.)
|
     
   |
|
Theorem | eqeqan12d 2115 |
A useful inference for substituting definitions into an equality.
(Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon,
25-May-2011.)
|
       
   |
|
Theorem | eqeqan12rd 2116 |
A useful inference for substituting definitions into an equality.
(Contributed by NM, 9-Aug-1994.)
|
       
   |
|
Theorem | eqtr 2117 |
Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring]
p. 13. (Contributed by NM, 25-Jan-2004.)
|
     |
|
Theorem | eqtr2 2118 |
A transitive law for class equality. (Contributed by NM, 20-May-2005.)
(Proof shortened by Andrew Salmon, 25-May-2011.)
|
     |
|
Theorem | eqtr3 2119 |
A transitive law for class equality. (Contributed by NM, 20-May-2005.)
|
     |
|
Theorem | eqtri 2120 |
An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
|
 |
|
Theorem | eqtr2i 2121 |
An equality transitivity inference. (Contributed by NM,
21-Feb-1995.)
|
 |
|
Theorem | eqtr3i 2122 |
An equality transitivity inference. (Contributed by NM, 6-May-1994.)
|
 |
|
Theorem | eqtr4i 2123 |
An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
|
 |
|
Theorem | 3eqtri 2124 |
An inference from three chained equalities. (Contributed by NM,
29-Aug-1993.)
|
 |
|
Theorem | 3eqtrri 2125 |
An inference from three chained equalities. (Contributed by NM,
3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|
 |
|
Theorem | 3eqtr2i 2126 |
An inference from three chained equalities. (Contributed by NM,
3-Aug-2006.)
|
 |
|
Theorem | 3eqtr2ri 2127 |
An inference from three chained equalities. (Contributed by NM,
3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|
 |
|
Theorem | 3eqtr3i 2128 |
An inference from three chained equalities. (Contributed by NM,
6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|
 |
|
Theorem | 3eqtr3ri 2129 |
An inference from three chained equalities. (Contributed by NM,
15-Aug-2004.)
|
 |
|
Theorem | 3eqtr4i 2130 |
An inference from three chained equalities. (Contributed by NM,
5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|
 |
|
Theorem | 3eqtr4ri 2131 |
An inference from three chained equalities. (Contributed by NM,
2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|
 |
|
Theorem | eqtrd 2132 |
An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|
       |
|
Theorem | eqtr2d 2133 |
An equality transitivity deduction. (Contributed by NM,
18-Oct-1999.)
|
       |
|
Theorem | eqtr3d 2134 |
An equality transitivity equality deduction. (Contributed by NM,
18-Jul-1995.)
|
       |
|
Theorem | eqtr4d 2135 |
An equality transitivity equality deduction. (Contributed by NM,
18-Jul-1995.)
|
       |
|
Theorem | 3eqtrd 2136 |
A deduction from three chained equalities. (Contributed by NM,
29-Oct-1995.)
|
         |
|
Theorem | 3eqtrrd 2137 |
A deduction from three chained equalities. (Contributed by NM,
4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|
         |
|
Theorem | 3eqtr2d 2138 |
A deduction from three chained equalities. (Contributed by NM,
4-Aug-2006.)
|
         |
|
Theorem | 3eqtr2rd 2139 |
A deduction from three chained equalities. (Contributed by NM,
4-Aug-2006.)
|
         |
|
Theorem | 3eqtr3d 2140 |
A deduction from three chained equalities. (Contributed by NM,
4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|
         |
|
Theorem | 3eqtr3rd 2141 |
A deduction from three chained equalities. (Contributed by NM,
14-Jan-2006.)
|
         |
|
Theorem | 3eqtr4d 2142 |
A deduction from three chained equalities. (Contributed by NM,
4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|
         |
|
Theorem | 3eqtr4rd 2143 |
A deduction from three chained equalities. (Contributed by NM,
21-Sep-1995.)
|
         |
|
Theorem | syl5eq 2144 |
An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|
     |
|
Theorem | syl5req 2145 |
An equality transitivity deduction. (Contributed by NM,
29-Mar-1998.)
|
     |
|
Theorem | syl5eqr 2146 |
An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|
     |
|
Theorem | syl5reqr 2147 |
An equality transitivity deduction. (Contributed by NM,
29-Mar-1998.)
|
     |
|
Theorem | syl6eq 2148 |
An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|
     |
|
Theorem | syl6req 2149 |
An equality transitivity deduction. (Contributed by NM,
29-Mar-1998.)
|
     |
|
Theorem | syl6eqr 2150 |
An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
|
     |
|
Theorem | syl6reqr 2151 |
An equality transitivity deduction. (Contributed by NM,
29-Mar-1998.)
|
     |
|
Theorem | sylan9eq 2152 |
An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
(Proof shortened by Andrew Salmon, 25-May-2011.)
|
         |
|
Theorem | sylan9req 2153 |
An equality transitivity deduction. (Contributed by NM,
23-Jun-2007.)
|
         |
|
Theorem | sylan9eqr 2154 |
An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
|
         |
|
Theorem | 3eqtr3g 2155 |
A chained equality inference, useful for converting from definitions.
(Contributed by NM, 15-Nov-1994.)
|
     |
|
Theorem | 3eqtr3a 2156 |
A chained equality inference, useful for converting from definitions.
(Contributed by Mario Carneiro, 6-Nov-2015.)
|
       |
|
Theorem | 3eqtr4g 2157 |
A chained equality inference, useful for converting to definitions.
(Contributed by NM, 5-Aug-1993.)
|
     |
|
Theorem | 3eqtr4a 2158 |
A chained equality inference, useful for converting to definitions.
(Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon,
25-May-2011.)
|
       |
|
Theorem | eq2tri 2159 |
A compound transitive inference for class equality. (Contributed by NM,
22-Jan-2004.)
|
  
        |
|
Theorem | eleq1w 2160 |
Weaker version of eleq1 2162 (but more general than elequ1 1658) not
depending on ax-ext 2082 nor df-cleq 2093. (Contributed by BJ,
24-Jun-2019.)
|
     |
|
Theorem | eleq2w 2161 |
Weaker version of eleq2 2163 (but more general than elequ2 1659) not
depending on ax-ext 2082 nor df-cleq 2093. (Contributed by BJ,
29-Sep-2019.)
|
     |
|
Theorem | eleq1 2162 |
Equality implies equivalence of membership. (Contributed by NM,
5-Aug-1993.)
|
     |
|
Theorem | eleq2 2163 |
Equality implies equivalence of membership. (Contributed by NM,
5-Aug-1993.)
|
     |
|
Theorem | eleq12 2164 |
Equality implies equivalence of membership. (Contributed by NM,
31-May-1999.)
|
       |
|
Theorem | eleq1i 2165 |
Inference from equality to equivalence of membership. (Contributed by
NM, 5-Aug-1993.)
|
   |
|
Theorem | eleq2i 2166 |
Inference from equality to equivalence of membership. (Contributed by
NM, 5-Aug-1993.)
|
   |
|
Theorem | eleq12i 2167 |
Inference from equality to equivalence of membership. (Contributed by
NM, 31-May-1994.)
|
   |
|
Theorem | eleq1d 2168 |
Deduction from equality to equivalence of membership. (Contributed by
NM, 5-Aug-1993.)
|
   
   |
|
Theorem | eleq2d 2169 |
Deduction from equality to equivalence of membership. (Contributed by
NM, 27-Dec-1993.)
|
   
   |
|
Theorem | eleq12d 2170 |
Deduction from equality to equivalence of membership. (Contributed by
NM, 31-May-1994.)
|
     
   |
|
Theorem | eleq1a 2171 |
A transitive-type law relating membership and equality. (Contributed by
NM, 9-Apr-1994.)
|
     |
|
Theorem | eqeltri 2172 |
Substitution of equal classes into membership relation. (Contributed by
NM, 5-Aug-1993.)
|
 |
|
Theorem | eqeltrri 2173 |
Substitution of equal classes into membership relation. (Contributed by
NM, 5-Aug-1993.)
|
 |
|
Theorem | eleqtri 2174 |
Substitution of equal classes into membership relation. (Contributed by
NM, 5-Aug-1993.)
|
 |
|
Theorem | eleqtrri 2175 |
Substitution of equal classes into membership relation. (Contributed by
NM, 5-Aug-1993.)
|
 |
|
Theorem | eqeltrd 2176 |
Substitution of equal classes into membership relation, deduction form.
(Contributed by Raph Levien, 10-Dec-2002.)
|
       |
|
Theorem | eqeltrrd 2177 |
Deduction that substitutes equal classes into membership. (Contributed
by NM, 14-Dec-2004.)
|
       |
|
Theorem | eleqtrd 2178 |
Deduction that substitutes equal classes into membership. (Contributed
by NM, 14-Dec-2004.)
|
       |
|
Theorem | eleqtrrd 2179 |
Deduction that substitutes equal classes into membership. (Contributed
by NM, 14-Dec-2004.)
|
       |
|
Theorem | 3eltr3i 2180 |
Substitution of equal classes into membership relation. (Contributed by
Mario Carneiro, 6-Jan-2017.)
|
 |
|
Theorem | 3eltr4i 2181 |
Substitution of equal classes into membership relation. (Contributed by
Mario Carneiro, 6-Jan-2017.)
|
 |
|
Theorem | 3eltr3d 2182 |
Substitution of equal classes into membership relation. (Contributed by
Mario Carneiro, 6-Jan-2017.)
|
         |
|
Theorem | 3eltr4d 2183 |
Substitution of equal classes into membership relation. (Contributed by
Mario Carneiro, 6-Jan-2017.)
|
         |
|
Theorem | 3eltr3g 2184 |
Substitution of equal classes into membership relation. (Contributed by
Mario Carneiro, 6-Jan-2017.)
|
     |
|
Theorem | 3eltr4g 2185 |
Substitution of equal classes into membership relation. (Contributed by
Mario Carneiro, 6-Jan-2017.)
|
     |
|
Theorem | syl5eqel 2186 |
B membership and equality inference. (Contributed by NM,
4-Jan-2006.)
|
     |
|
Theorem | syl5eqelr 2187 |
B membership and equality inference. (Contributed by NM,
4-Jan-2006.)
|
     |
|
Theorem | syl5eleq 2188 |
B membership and equality inference. (Contributed by NM,
4-Jan-2006.)
|
     |
|
Theorem | syl5eleqr 2189 |
B membership and equality inference. (Contributed by NM,
4-Jan-2006.)
|
     |
|
Theorem | syl6eqel 2190 |
A membership and equality inference. (Contributed by NM,
4-Jan-2006.)
|
     |
|
Theorem | syl6eqelr 2191 |
A membership and equality inference. (Contributed by NM,
4-Jan-2006.)
|
     |
|
Theorem | syl6eleq 2192 |
A membership and equality inference. (Contributed by NM,
4-Jan-2006.)
|
     |
|
Theorem | syl6eleqr 2193 |
A membership and equality inference. (Contributed by NM,
24-Apr-2005.)
|
     |
|
Theorem | eleq2s 2194 |
Substitution of equal classes into a membership antecedent.
(Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|
  
  |
|
Theorem | eqneltrd 2195 |
If a class is not an element of another class, an equal class is also
not an element. Deduction form. (Contributed by David Moews,
1-May-2017.)
|
    
  |
|
Theorem | eqneltrrd 2196 |
If a class is not an element of another class, an equal class is also
not an element. Deduction form. (Contributed by David Moews,
1-May-2017.)
|
    
  |
|
Theorem | neleqtrd 2197 |
If a class is not an element of another class, it is also not an element
of an equal class. Deduction form. (Contributed by David Moews,
1-May-2017.)
|
       |
|
Theorem | neleqtrrd 2198 |
If a class is not an element of another class, it is also not an element
of an equal class. Deduction form. (Contributed by David Moews,
1-May-2017.)
|
       |
|
Theorem | cleqh 2199* |
Establish equality between classes, using bound-variable hypotheses
instead of distinct variable conditions. See also cleqf 2264.
(Contributed by NM, 5-Aug-1993.)
|
   
     
   |
|
Theorem | nelneq 2200 |
A way of showing two classes are not equal. (Contributed by NM,
1-Apr-1997.)
|
  
  |