HomeHome Intuitionistic Logic Explorer
Theorem List (p. 23 of 153)
< Previous  Next >
Bad symbols? Try the
GIF version.

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

Theorem List for Intuitionistic Logic Explorer - 2201-2300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremeqeq2d 2201 Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐶 = 𝐴𝐶 = 𝐵))
 
Theoremeqeq12 2202 Equality relationship among 4 classes. (Contributed by NM, 3-Aug-1994.)
((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
 
Theoremeqeq12i 2203 A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
𝐴 = 𝐵    &   𝐶 = 𝐷       (𝐴 = 𝐶𝐵 = 𝐷)
 
Theoremeqeq12d 2204 A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
 
Theoremeqeqan12d 2205 A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜓𝐶 = 𝐷)       ((𝜑𝜓) → (𝐴 = 𝐶𝐵 = 𝐷))
 
Theoremeqeqan12rd 2206 A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.)
(𝜑𝐴 = 𝐵)    &   (𝜓𝐶 = 𝐷)       ((𝜓𝜑) → (𝐴 = 𝐶𝐵 = 𝐷))
 
Theoremeqtr 2207 Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.)
((𝐴 = 𝐵𝐵 = 𝐶) → 𝐴 = 𝐶)
 
Theoremeqtr2 2208 A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
((𝐴 = 𝐵𝐴 = 𝐶) → 𝐵 = 𝐶)
 
Theoremeqtr3 2209 A transitive law for class equality. (Contributed by NM, 20-May-2005.)
((𝐴 = 𝐶𝐵 = 𝐶) → 𝐴 = 𝐵)
 
Theoremeqtri 2210 An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵    &   𝐵 = 𝐶       𝐴 = 𝐶
 
Theoremeqtr2i 2211 An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
𝐴 = 𝐵    &   𝐵 = 𝐶       𝐶 = 𝐴
 
Theoremeqtr3i 2212 An equality transitivity inference. (Contributed by NM, 6-May-1994.)
𝐴 = 𝐵    &   𝐴 = 𝐶       𝐵 = 𝐶
 
Theoremeqtr4i 2213 An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵    &   𝐶 = 𝐵       𝐴 = 𝐶
 
Theorem3eqtri 2214 An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
𝐴 = 𝐵    &   𝐵 = 𝐶    &   𝐶 = 𝐷       𝐴 = 𝐷
 
Theorem3eqtrri 2215 An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
𝐴 = 𝐵    &   𝐵 = 𝐶    &   𝐶 = 𝐷       𝐷 = 𝐴
 
Theorem3eqtr2i 2216 An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)
𝐴 = 𝐵    &   𝐶 = 𝐵    &   𝐶 = 𝐷       𝐴 = 𝐷
 
Theorem3eqtr2ri 2217 An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
𝐴 = 𝐵    &   𝐶 = 𝐵    &   𝐶 = 𝐷       𝐷 = 𝐴
 
Theorem3eqtr3i 2218 An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
𝐴 = 𝐵    &   𝐴 = 𝐶    &   𝐵 = 𝐷       𝐶 = 𝐷
 
Theorem3eqtr3ri 2219 An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
𝐴 = 𝐵    &   𝐴 = 𝐶    &   𝐵 = 𝐷       𝐷 = 𝐶
 
Theorem3eqtr4i 2220 An inference from three chained equalities. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
𝐴 = 𝐵    &   𝐶 = 𝐴    &   𝐷 = 𝐵       𝐶 = 𝐷
 
Theorem3eqtr4ri 2221 An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
𝐴 = 𝐵    &   𝐶 = 𝐴    &   𝐷 = 𝐵       𝐷 = 𝐶
 
Theoremeqtrd 2222 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐵 = 𝐶)       (𝜑𝐴 = 𝐶)
 
Theoremeqtr2d 2223 An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐵 = 𝐶)       (𝜑𝐶 = 𝐴)
 
Theoremeqtr3d 2224 An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐴 = 𝐶)       (𝜑𝐵 = 𝐶)
 
Theoremeqtr4d 2225 An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐵)       (𝜑𝐴 = 𝐶)
 
Theorem3eqtrd 2226 A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐵 = 𝐶)    &   (𝜑𝐶 = 𝐷)       (𝜑𝐴 = 𝐷)
 
Theorem3eqtrrd 2227 A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐵 = 𝐶)    &   (𝜑𝐶 = 𝐷)       (𝜑𝐷 = 𝐴)
 
Theorem3eqtr2d 2228 A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑𝐴 = 𝐷)
 
Theorem3eqtr2rd 2229 A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑𝐷 = 𝐴)
 
Theorem3eqtr3d 2230 A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐴 = 𝐶)    &   (𝜑𝐵 = 𝐷)       (𝜑𝐶 = 𝐷)
 
Theorem3eqtr3rd 2231 A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐴 = 𝐶)    &   (𝜑𝐵 = 𝐷)       (𝜑𝐷 = 𝐶)
 
Theorem3eqtr4d 2232 A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐴)    &   (𝜑𝐷 = 𝐵)       (𝜑𝐶 = 𝐷)
 
Theorem3eqtr4rd 2233 A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐴)    &   (𝜑𝐷 = 𝐵)       (𝜑𝐷 = 𝐶)
 
Theoremeqtrid 2234 An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)
𝐴 = 𝐵    &   (𝜑𝐵 = 𝐶)       (𝜑𝐴 = 𝐶)
 
Theoremeqtr2id 2235 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
𝐴 = 𝐵    &   (𝜑𝐵 = 𝐶)       (𝜑𝐶 = 𝐴)
 
Theoremeqtr3id 2236 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
𝐵 = 𝐴    &   (𝜑𝐵 = 𝐶)       (𝜑𝐴 = 𝐶)
 
Theoremeqtr3di 2237 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
(𝜑𝐴 = 𝐵)    &   𝐴 = 𝐶       (𝜑𝐵 = 𝐶)
 
Theoremeqtrdi 2238 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
(𝜑𝐴 = 𝐵)    &   𝐵 = 𝐶       (𝜑𝐴 = 𝐶)
 
Theoremeqtr2di 2239 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
(𝜑𝐴 = 𝐵)    &   𝐵 = 𝐶       (𝜑𝐶 = 𝐴)
 
Theoremeqtr4di 2240 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
(𝜑𝐴 = 𝐵)    &   𝐶 = 𝐵       (𝜑𝐴 = 𝐶)
 
Theoremeqtr4id 2241 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
𝐴 = 𝐵    &   (𝜑𝐶 = 𝐵)       (𝜑𝐴 = 𝐶)
 
Theoremsylan9eq 2242 An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜓𝐵 = 𝐶)       ((𝜑𝜓) → 𝐴 = 𝐶)
 
Theoremsylan9req 2243 An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
(𝜑𝐵 = 𝐴)    &   (𝜓𝐵 = 𝐶)       ((𝜑𝜓) → 𝐴 = 𝐶)
 
Theoremsylan9eqr 2244 An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
(𝜑𝐴 = 𝐵)    &   (𝜓𝐵 = 𝐶)       ((𝜓𝜑) → 𝐴 = 𝐶)
 
Theorem3eqtr3g 2245 A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)
(𝜑𝐴 = 𝐵)    &   𝐴 = 𝐶    &   𝐵 = 𝐷       (𝜑𝐶 = 𝐷)
 
Theorem3eqtr3a 2246 A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)
𝐴 = 𝐵    &   (𝜑𝐴 = 𝐶)    &   (𝜑𝐵 = 𝐷)       (𝜑𝐶 = 𝐷)
 
Theorem3eqtr4g 2247 A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.)
(𝜑𝐴 = 𝐵)    &   𝐶 = 𝐴    &   𝐷 = 𝐵       (𝜑𝐶 = 𝐷)
 
Theorem3eqtr4a 2248 A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
𝐴 = 𝐵    &   (𝜑𝐶 = 𝐴)    &   (𝜑𝐷 = 𝐵)       (𝜑𝐶 = 𝐷)
 
Theoremeq2tri 2249 A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004.)
(𝐴 = 𝐶𝐷 = 𝐹)    &   (𝐵 = 𝐷𝐶 = 𝐺)       ((𝐴 = 𝐶𝐵 = 𝐹) ↔ (𝐵 = 𝐷𝐴 = 𝐺))
 
Theoremeleq1w 2250 Weaker version of eleq1 2252 (but more general than elequ1 2164) not depending on ax-ext 2171 nor df-cleq 2182. (Contributed by BJ, 24-Jun-2019.)
(𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
 
Theoremeleq2w 2251 Weaker version of eleq2 2253 (but more general than elequ2 2165) not depending on ax-ext 2171 nor df-cleq 2182. (Contributed by BJ, 29-Sep-2019.)
(𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))
 
Theoremeleq1 2252 Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
(𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
 
Theoremeleq2 2253 Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
(𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
 
Theoremeleq12 2254 Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)
((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶𝐵𝐷))
 
Theoremeleq1i 2255 Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵       (𝐴𝐶𝐵𝐶)
 
Theoremeleq2i 2256 Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵       (𝐶𝐴𝐶𝐵)
 
Theoremeleq12i 2257 Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
𝐴 = 𝐵    &   𝐶 = 𝐷       (𝐴𝐶𝐵𝐷)
 
Theoremeleq1d 2258 Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐴𝐶𝐵𝐶))
 
Theoremeleq2d 2259 Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐶𝐴𝐶𝐵))
 
Theoremeleq12d 2260 Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑 → (𝐴𝐶𝐵𝐷))
 
Theoremeleq1a 2261 A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
(𝐴𝐵 → (𝐶 = 𝐴𝐶𝐵))
 
Theoremeqeltri 2262 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵    &   𝐵𝐶       𝐴𝐶
 
Theoremeqeltrri 2263 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵    &   𝐴𝐶       𝐵𝐶
 
Theoremeleqtri 2264 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
𝐴𝐵    &   𝐵 = 𝐶       𝐴𝐶
 
Theoremeleqtrri 2265 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
𝐴𝐵    &   𝐶 = 𝐵       𝐴𝐶
 
Theoremeqeltrd 2266 Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐵𝐶)       (𝜑𝐴𝐶)
 
Theoremeqeltrrd 2267 Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐴𝐶)       (𝜑𝐵𝐶)
 
Theoremeleqtrd 2268 Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
(𝜑𝐴𝐵)    &   (𝜑𝐵 = 𝐶)       (𝜑𝐴𝐶)
 
Theoremeleqtrrd 2269 Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
(𝜑𝐴𝐵)    &   (𝜑𝐶 = 𝐵)       (𝜑𝐴𝐶)
 
Theorem3eltr3i 2270 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
𝐴𝐵    &   𝐴 = 𝐶    &   𝐵 = 𝐷       𝐶𝐷
 
Theorem3eltr4i 2271 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
𝐴𝐵    &   𝐶 = 𝐴    &   𝐷 = 𝐵       𝐶𝐷
 
Theorem3eltr3d 2272 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
(𝜑𝐴𝐵)    &   (𝜑𝐴 = 𝐶)    &   (𝜑𝐵 = 𝐷)       (𝜑𝐶𝐷)
 
Theorem3eltr4d 2273 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
(𝜑𝐴𝐵)    &   (𝜑𝐶 = 𝐴)    &   (𝜑𝐷 = 𝐵)       (𝜑𝐶𝐷)
 
Theorem3eltr3g 2274 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
(𝜑𝐴𝐵)    &   𝐴 = 𝐶    &   𝐵 = 𝐷       (𝜑𝐶𝐷)
 
Theorem3eltr4g 2275 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
(𝜑𝐴𝐵)    &   𝐶 = 𝐴    &   𝐷 = 𝐵       (𝜑𝐶𝐷)
 
Theoremeqeltrid 2276 B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
𝐴 = 𝐵    &   (𝜑𝐵𝐶)       (𝜑𝐴𝐶)
 
Theoremeqeltrrid 2277 B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
𝐵 = 𝐴    &   (𝜑𝐵𝐶)       (𝜑𝐴𝐶)
 
Theoremeleqtrid 2278 B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
𝐴𝐵    &   (𝜑𝐵 = 𝐶)       (𝜑𝐴𝐶)
 
Theoremeleqtrrid 2279 B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
𝐴𝐵    &   (𝜑𝐶 = 𝐵)       (𝜑𝐴𝐶)
 
Theoremeqeltrdi 2280 A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
(𝜑𝐴 = 𝐵)    &   𝐵𝐶       (𝜑𝐴𝐶)
 
Theoremeqeltrrdi 2281 A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
(𝜑𝐵 = 𝐴)    &   𝐵𝐶       (𝜑𝐴𝐶)
 
Theoremeleqtrdi 2282 A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
(𝜑𝐴𝐵)    &   𝐵 = 𝐶       (𝜑𝐴𝐶)
 
Theoremeleqtrrdi 2283 A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
(𝜑𝐴𝐵)    &   𝐶 = 𝐵       (𝜑𝐴𝐶)
 
Theoremeleq2s 2284 Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(𝐴𝐵𝜑)    &   𝐶 = 𝐵       (𝐴𝐶𝜑)
 
Theoremeqneltrd 2285 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.)
(𝜑𝐴 = 𝐵)    &   (𝜑 → ¬ 𝐵𝐶)       (𝜑 → ¬ 𝐴𝐶)
 
Theoremeqneltrrd 2286 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.)
(𝜑𝐴 = 𝐵)    &   (𝜑 → ¬ 𝐴𝐶)       (𝜑 → ¬ 𝐵𝐶)
 
Theoremneleqtrd 2287 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.)
(𝜑 → ¬ 𝐶𝐴)    &   (𝜑𝐴 = 𝐵)       (𝜑 → ¬ 𝐶𝐵)
 
Theoremneleqtrrd 2288 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.)
(𝜑 → ¬ 𝐶𝐵)    &   (𝜑𝐴 = 𝐵)       (𝜑 → ¬ 𝐶𝐴)
 
Theoremcleqh 2289* Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqf 2357. (Contributed by NM, 5-Aug-1993.)
(𝑦𝐴 → ∀𝑥 𝑦𝐴)    &   (𝑦𝐵 → ∀𝑥 𝑦𝐵)       (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
 
Theoremnelneq 2290 A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997.)
((𝐴𝐶 ∧ ¬ 𝐵𝐶) → ¬ 𝐴 = 𝐵)
 
Theoremnelneq2 2291 A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002.)
((𝐴𝐵 ∧ ¬ 𝐴𝐶) → ¬ 𝐵 = 𝐶)
 
Theoremeqsb1lem 2292* Lemma for eqsb1 2293. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
([𝑦 / 𝑥]𝑥 = 𝐴𝑦 = 𝐴)
 
Theoremeqsb1 2293* Substitution for the left-hand side in an equality. Class version of equsb3 1963. (Contributed by Rodolfo Medina, 28-Apr-2010.)
([𝑦 / 𝑥]𝑥 = 𝐴𝑦 = 𝐴)
 
Theoremclelsb1 2294* Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2167). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
([𝑦 / 𝑥]𝑥𝐴𝑦𝐴)
 
Theoremclelsb2 2295* Substitution for the second argument of the membership predicate in an atomic formula (class version of elsb2 2168). (Contributed by Jim Kingdon, 22-Nov-2018.)
([𝑦 / 𝑥]𝐴𝑥𝐴𝑦)
 
Theoremhbxfreq 2296 A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1483 for equivalence version. (Contributed by NM, 21-Aug-2007.)
𝐴 = 𝐵    &   (𝑦𝐵 → ∀𝑥 𝑦𝐵)       (𝑦𝐴 → ∀𝑥 𝑦𝐴)
 
Theoremhblem 2297* Change the free variable of a hypothesis builder. (Contributed by NM, 5-Aug-1993.) (Revised by Andrew Salmon, 11-Jul-2011.)
(𝑦𝐴 → ∀𝑥 𝑦𝐴)       (𝑧𝐴 → ∀𝑥 𝑧𝐴)
 
Theoremabeq2 2298* Equality of a class variable and a class abstraction (also called a class builder). Theorem 5.1 of [Quine] p. 34. This theorem shows the relationship between expressions with class abstractions and expressions with class variables. Note that abbi 2303 and its relatives are among those useful for converting theorems with class variables to equivalent theorems with wff variables, by first substituting a class abstraction for each class variable.

Class variables can always be eliminated from a theorem to result in an equivalent theorem with wff variables, and vice-versa. The idea is roughly as follows. To convert a theorem with a wff variable 𝜑 (that has a free variable 𝑥) to a theorem with a class variable 𝐴, we substitute 𝑥𝐴 for 𝜑 throughout and simplify, where 𝐴 is a new class variable not already in the wff. Conversely, to convert a theorem with a class variable 𝐴 to one with 𝜑, we substitute {𝑥𝜑} for 𝐴 throughout and simplify, where 𝑥 and 𝜑 are new set and wff variables not already in the wff. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. (Contributed by NM, 5-Aug-1993.)

(𝐴 = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝜑))
 
Theoremabeq1 2299* Equality of a class variable and a class abstraction. (Contributed by NM, 20-Aug-1993.)
({𝑥𝜑} = 𝐴 ↔ ∀𝑥(𝜑𝑥𝐴))
 
Theoremabeq2i 2300 Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.)
𝐴 = {𝑥𝜑}       (𝑥𝐴𝜑)
    < 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-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15294
  Copyright terms: Public domain < Previous  Next >