HomeHome Intuitionistic Logic Explorer
Theorem List (p. 22 of 129)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 2101-2200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremeqidd 2101 Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)
 |-  ( ph  ->  A  =  A )
 
Theoremeqcom 2102 Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 5-Aug-1993.)
 |-  ( A  =  B  <->  B  =  A )
 
Theoremeqcoms 2103 Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 5-Aug-1993.)
 |-  ( A  =  B  -> 
 ph )   =>    |-  ( B  =  A  -> 
 ph )
 
Theoremeqcomi 2104 Inference from commutative law for class equality. (Contributed by NM, 5-Aug-1993.)
 |-  A  =  B   =>    |-  B  =  A
 
Theoremeqcomd 2105 Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.)
 |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  B  =  A )
 
Theoremeqeq1 2106 Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
 |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
 
Theoremeqeq1i 2107 Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
 |-  A  =  B   =>    |-  ( A  =  C 
 <->  B  =  C )
 
Theoremeqeq1d 2108 Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
 |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  ( A  =  C  <->  B  =  C ) )
 
Theoremeqeq2 2109 Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
 |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
 
Theoremeqeq2i 2110 Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
 |-  A  =  B   =>    |-  ( C  =  A 
 <->  C  =  B )
 
Theoremeqeq2d 2111 Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
 |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  ( C  =  A  <->  C  =  B ) )
 
Theoremeqeq12 2112 Equality relationship among 4 classes. (Contributed by NM, 3-Aug-1994.)
 |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C 
 <->  B  =  D ) )
 
Theoremeqeq12i 2113 A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  A  =  B   &    |-  C  =  D   =>    |-  ( A  =  C  <->  B  =  D )
 
Theoremeqeq12d 2114 A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  C  =  D )   =>    |-  ( ph  ->  ( A  =  C  <->  B  =  D ) )
 
Theoremeqeqan12d 2115 A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ps  ->  C  =  D )   =>    |-  ( ( ph  /\ 
 ps )  ->  ( A  =  C  <->  B  =  D ) )
 
Theoremeqeqan12rd 2116 A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ps  ->  C  =  D )   =>    |-  ( ( ps 
 /\  ph )  ->  ( A  =  C  <->  B  =  D ) )
 
Theoremeqtr 2117 Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.)
 |-  ( ( A  =  B  /\  B  =  C )  ->  A  =  C )
 
Theoremeqtr2 2118 A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  ( ( A  =  B  /\  A  =  C )  ->  B  =  C )
 
Theoremeqtr3 2119 A transitive law for class equality. (Contributed by NM, 20-May-2005.)
 |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )
 
Theoremeqtri 2120 An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
 |-  A  =  B   &    |-  B  =  C   =>    |-  A  =  C
 
Theoremeqtr2i 2121 An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
 |-  A  =  B   &    |-  B  =  C   =>    |-  C  =  A
 
Theoremeqtr3i 2122 An equality transitivity inference. (Contributed by NM, 6-May-1994.)
 |-  A  =  B   &    |-  A  =  C   =>    |-  B  =  C
 
Theoremeqtr4i 2123 An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
 |-  A  =  B   &    |-  C  =  B   =>    |-  A  =  C
 
Theorem3eqtri 2124 An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
 |-  A  =  B   &    |-  B  =  C   &    |-  C  =  D   =>    |-  A  =  D
 
Theorem3eqtrri 2125 An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  A  =  B   &    |-  B  =  C   &    |-  C  =  D   =>    |-  D  =  A
 
Theorem3eqtr2i 2126 An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)
 |-  A  =  B   &    |-  C  =  B   &    |-  C  =  D   =>    |-  A  =  D
 
Theorem3eqtr2ri 2127 An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  A  =  B   &    |-  C  =  B   &    |-  C  =  D   =>    |-  D  =  A
 
Theorem3eqtr3i 2128 An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  A  =  B   &    |-  A  =  C   &    |-  B  =  D   =>    |-  C  =  D
 
Theorem3eqtr3ri 2129 An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
 |-  A  =  B   &    |-  A  =  C   &    |-  B  =  D   =>    |-  D  =  C
 
Theorem3eqtr4i 2130 An inference from three chained equalities. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  A  =  B   &    |-  C  =  A   &    |-  D  =  B   =>    |-  C  =  D
 
Theorem3eqtr4ri 2131 An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  A  =  B   &    |-  C  =  A   &    |-  D  =  B   =>    |-  D  =  C
 
Theoremeqtrd 2132 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  B  =  C )   =>    |-  ( ph  ->  A  =  C )
 
Theoremeqtr2d 2133 An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  B  =  C )   =>    |-  ( ph  ->  C  =  A )
 
Theoremeqtr3d 2134 An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  A  =  C )   =>    |-  ( ph  ->  B  =  C )
 
Theoremeqtr4d 2135 An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  C  =  B )   =>    |-  ( ph  ->  A  =  C )
 
Theorem3eqtrd 2136 A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  B  =  C )   &    |-  ( ph  ->  C  =  D )   =>    |-  ( ph  ->  A  =  D )
 
Theorem3eqtrrd 2137 A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  B  =  C )   &    |-  ( ph  ->  C  =  D )   =>    |-  ( ph  ->  D  =  A )
 
Theorem3eqtr2d 2138 A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  C  =  B )   &    |-  ( ph  ->  C  =  D )   =>    |-  ( ph  ->  A  =  D )
 
Theorem3eqtr2rd 2139 A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  C  =  B )   &    |-  ( ph  ->  C  =  D )   =>    |-  ( ph  ->  D  =  A )
 
Theorem3eqtr3d 2140 A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  A  =  C )   &    |-  ( ph  ->  B  =  D )   =>    |-  ( ph  ->  C  =  D )
 
Theorem3eqtr3rd 2141 A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  A  =  C )   &    |-  ( ph  ->  B  =  D )   =>    |-  ( ph  ->  D  =  C )
 
Theorem3eqtr4d 2142 A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  C  =  A )   &    |-  ( ph  ->  D  =  B )   =>    |-  ( ph  ->  C  =  D )
 
Theorem3eqtr4rd 2143 A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  C  =  A )   &    |-  ( ph  ->  D  =  B )   =>    |-  ( ph  ->  D  =  C )
 
Theoremsyl5eq 2144 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
 |-  A  =  B   &    |-  ( ph  ->  B  =  C )   =>    |-  ( ph  ->  A  =  C )
 
Theoremsyl5req 2145 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
 |-  A  =  B   &    |-  ( ph  ->  B  =  C )   =>    |-  ( ph  ->  C  =  A )
 
Theoremsyl5eqr 2146 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
 |-  B  =  A   &    |-  ( ph  ->  B  =  C )   =>    |-  ( ph  ->  A  =  C )
 
Theoremsyl5reqr 2147 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
 |-  B  =  A   &    |-  ( ph  ->  B  =  C )   =>    |-  ( ph  ->  C  =  A )
 
Theoremsyl6eq 2148 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
 |-  ( ph  ->  A  =  B )   &    |-  B  =  C   =>    |-  ( ph  ->  A  =  C )
 
Theoremsyl6req 2149 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
 |-  ( ph  ->  A  =  B )   &    |-  B  =  C   =>    |-  ( ph  ->  C  =  A )
 
Theoremsyl6eqr 2150 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
 |-  ( ph  ->  A  =  B )   &    |-  C  =  B   =>    |-  ( ph  ->  A  =  C )
 
Theoremsyl6reqr 2151 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
 |-  ( ph  ->  A  =  B )   &    |-  C  =  B   =>    |-  ( ph  ->  C  =  A )
 
Theoremsylan9eq 2152 An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ps  ->  B  =  C )   =>    |-  ( ( ph  /\ 
 ps )  ->  A  =  C )
 
Theoremsylan9req 2153 An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
 |-  ( ph  ->  B  =  A )   &    |-  ( ps  ->  B  =  C )   =>    |-  ( ( ph  /\ 
 ps )  ->  A  =  C )
 
Theoremsylan9eqr 2154 An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ps  ->  B  =  C )   =>    |-  ( ( ps 
 /\  ph )  ->  A  =  C )
 
Theorem3eqtr3g 2155 A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)
 |-  ( ph  ->  A  =  B )   &    |-  A  =  C   &    |-  B  =  D   =>    |-  ( ph  ->  C  =  D )
 
Theorem3eqtr3a 2156 A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)
 |-  A  =  B   &    |-  ( ph  ->  A  =  C )   &    |-  ( ph  ->  B  =  D )   =>    |-  ( ph  ->  C  =  D )
 
Theorem3eqtr4g 2157 A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.)
 |-  ( ph  ->  A  =  B )   &    |-  C  =  A   &    |-  D  =  B   =>    |-  ( ph  ->  C  =  D )
 
Theorem3eqtr4a 2158 A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  A  =  B   &    |-  ( ph  ->  C  =  A )   &    |-  ( ph  ->  D  =  B )   =>    |-  ( ph  ->  C  =  D )
 
Theoremeq2tri 2159 A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004.)
 |-  ( A  =  C  ->  D  =  F )   &    |-  ( B  =  D  ->  C  =  G )   =>    |-  ( ( A  =  C  /\  B  =  F ) 
 <->  ( B  =  D  /\  A  =  G ) )
 
Theoremeleq1w 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.)
 |-  ( x  =  y 
 ->  ( x  e.  A  <->  y  e.  A ) )
 
Theoremeleq2w 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.)
 |-  ( x  =  y 
 ->  ( A  e.  x  <->  A  e.  y ) )
 
Theoremeleq1 2162 Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
 |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
 
Theoremeleq2 2163 Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
 |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
 
Theoremeleq12 2164 Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)
 |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  e.  C 
 <->  B  e.  D ) )
 
Theoremeleq1i 2165 Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
 |-  A  =  B   =>    |-  ( A  e.  C 
 <->  B  e.  C )
 
Theoremeleq2i 2166 Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
 |-  A  =  B   =>    |-  ( C  e.  A 
 <->  C  e.  B )
 
Theoremeleq12i 2167 Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
 |-  A  =  B   &    |-  C  =  D   =>    |-  ( A  e.  C  <->  B  e.  D )
 
Theoremeleq1d 2168 Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
 |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  ( A  e.  C  <->  B  e.  C ) )
 
Theoremeleq2d 2169 Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)
 |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  ( C  e.  A  <->  C  e.  B ) )
 
Theoremeleq12d 2170 Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  C  =  D )   =>    |-  ( ph  ->  ( A  e.  C  <->  B  e.  D ) )
 
Theoremeleq1a 2171 A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
 |-  ( A  e.  B  ->  ( C  =  A  ->  C  e.  B ) )
 
Theoremeqeltri 2172 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
 |-  A  =  B   &    |-  B  e.  C   =>    |-  A  e.  C
 
Theoremeqeltrri 2173 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
 |-  A  =  B   &    |-  A  e.  C   =>    |-  B  e.  C
 
Theoremeleqtri 2174 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
 |-  A  e.  B   &    |-  B  =  C   =>    |-  A  e.  C
 
Theoremeleqtrri 2175 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
 |-  A  e.  B   &    |-  C  =  B   =>    |-  A  e.  C
 
Theoremeqeltrd 2176 Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  B  e.  C )   =>    |-  ( ph  ->  A  e.  C )
 
Theoremeqeltrrd 2177 Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  A  e.  C )   =>    |-  ( ph  ->  B  e.  C )
 
Theoremeleqtrd 2178 Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
 |-  ( ph  ->  A  e.  B )   &    |-  ( ph  ->  B  =  C )   =>    |-  ( ph  ->  A  e.  C )
 
Theoremeleqtrrd 2179 Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
 |-  ( ph  ->  A  e.  B )   &    |-  ( ph  ->  C  =  B )   =>    |-  ( ph  ->  A  e.  C )
 
Theorem3eltr3i 2180 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
 |-  A  e.  B   &    |-  A  =  C   &    |-  B  =  D   =>    |-  C  e.  D
 
Theorem3eltr4i 2181 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
 |-  A  e.  B   &    |-  C  =  A   &    |-  D  =  B   =>    |-  C  e.  D
 
Theorem3eltr3d 2182 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
 |-  ( ph  ->  A  e.  B )   &    |-  ( ph  ->  A  =  C )   &    |-  ( ph  ->  B  =  D )   =>    |-  ( ph  ->  C  e.  D )
 
Theorem3eltr4d 2183 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
 |-  ( ph  ->  A  e.  B )   &    |-  ( ph  ->  C  =  A )   &    |-  ( ph  ->  D  =  B )   =>    |-  ( ph  ->  C  e.  D )
 
Theorem3eltr3g 2184 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
 |-  ( ph  ->  A  e.  B )   &    |-  A  =  C   &    |-  B  =  D   =>    |-  ( ph  ->  C  e.  D )
 
Theorem3eltr4g 2185 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
 |-  ( ph  ->  A  e.  B )   &    |-  C  =  A   &    |-  D  =  B   =>    |-  ( ph  ->  C  e.  D )
 
Theoremsyl5eqel 2186 B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
 |-  A  =  B   &    |-  ( ph  ->  B  e.  C )   =>    |-  ( ph  ->  A  e.  C )
 
Theoremsyl5eqelr 2187 B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
 |-  B  =  A   &    |-  ( ph  ->  B  e.  C )   =>    |-  ( ph  ->  A  e.  C )
 
Theoremsyl5eleq 2188 B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
 |-  A  e.  B   &    |-  ( ph  ->  B  =  C )   =>    |-  ( ph  ->  A  e.  C )
 
Theoremsyl5eleqr 2189 B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
 |-  A  e.  B   &    |-  ( ph  ->  C  =  B )   =>    |-  ( ph  ->  A  e.  C )
 
Theoremsyl6eqel 2190 A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
 |-  ( ph  ->  A  =  B )   &    |-  B  e.  C   =>    |-  ( ph  ->  A  e.  C )
 
Theoremsyl6eqelr 2191 A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
 |-  ( ph  ->  B  =  A )   &    |-  B  e.  C   =>    |-  ( ph  ->  A  e.  C )
 
Theoremsyl6eleq 2192 A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
 |-  ( ph  ->  A  e.  B )   &    |-  B  =  C   =>    |-  ( ph  ->  A  e.  C )
 
Theoremsyl6eleqr 2193 A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
 |-  ( ph  ->  A  e.  B )   &    |-  C  =  B   =>    |-  ( ph  ->  A  e.  C )
 
Theoremeleq2s 2194 Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
 |-  ( A  e.  B  -> 
 ph )   &    |-  C  =  B   =>    |-  ( A  e.  C  ->  ph )
 
Theoremeqneltrd 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.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  -.  B  e.  C )   =>    |-  ( ph  ->  -.  A  e.  C )
 
Theoremeqneltrrd 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.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  -.  A  e.  C )   =>    |-  ( ph  ->  -.  B  e.  C )
 
Theoremneleqtrd 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.)
 |-  ( ph  ->  -.  C  e.  A )   &    |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  -.  C  e.  B )
 
Theoremneleqtrrd 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.)
 |-  ( ph  ->  -.  C  e.  B )   &    |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  -.  C  e.  A )
 
Theoremcleqh 2199* Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqf 2264. (Contributed by NM, 5-Aug-1993.)
 |-  ( y  e.  A  ->  A. x  y  e.  A )   &    |-  ( y  e.  B  ->  A. x  y  e.  B )   =>    |-  ( A  =  B 
 <-> 
 A. x ( x  e.  A  <->  x  e.  B ) )
 
Theoremnelneq 2200 A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997.)
 |-  ( ( A  e.  C  /\  -.  B  e.  C )  ->  -.  A  =  B )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12832
  Copyright terms: Public domain < Previous  Next >