Home | Metamath
Proof Explorer Theorem List (p. 425 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29659) |
Hilbert Space Explorer
(29660-31182) |
Users' Mathboxes
(31183-46998) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | binomcxplemnotnn0 42401* |
Lemma for binomcxp 42402. When πΆ is not a nonnegative integer, the
generalized sum in binomcxplemnn0 42394 βwhich we will call π
βis a convergent power series: its base π is always of
smaller absolute value than the radius of convergence.
pserdv2 25712 gives the derivative of π, which by dvradcnv 25703 also converges in that radius. When π΄ is fixed at one, (π΄ + π) times that derivative equals (πΆ Β· π) and fraction (π / ((π΄ + π)βππΆ)) is always defined with derivative zero, so the fraction is a constantβspecifically one, because ((1 + 0)βππΆ) = 1. Thus ((1 + π)βππΆ) = (πβπ). Finally, let π be (π΅ / π΄), and multiply both the binomial ((1 + (π΅ / π΄))βππΆ) and the sum (πβ(π΅ / π΄)) by (π΄βππΆ) to get the result. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β) & β’ (π β (absβπ΅) < (absβπ΄)) & β’ (π β πΆ β β) & β’ πΉ = (π β β0 β¦ (πΆCππ)) & β’ π = (π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) & β’ π = sup({π β β β£ seq0( + , (πβπ)) β dom β }, β*, < ) & β’ πΈ = (π β β β¦ (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1))))) & β’ π· = (β‘abs β (0[,)π )) & β’ π = (π β π· β¦ Ξ£π β β0 ((πβπ)βπ)) β β’ ((π β§ Β¬ πΆ β β0) β ((π΄ + π΅)βππΆ) = Ξ£π β β0 ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) | ||
Theorem | binomcxp 42402* | Generalize the binomial theorem binom 15650 to positive real summand π΄, real summand π΅, and complex exponent πΆ. Proof in https://en.wikibooks.org/wiki/Advanced_Calculus 15650; see also https://en.wikipedia.org/wiki/Binomial_series 15650, https://en.wikipedia.org/wiki/Binomial_theorem 15650 (sections "Newton's generalized binomial theorem" and "Future generalizations"), and proof "General Binomial Theorem" in https://proofwiki.org/wiki/Binomial_Theorem 15650. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β) & β’ (π β (absβπ΅) < (absβπ΄)) & β’ (π β πΆ β β) β β’ (π β ((π΄ + π΅)βππΆ) = Ξ£π β β0 ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) | ||
Theorem | pm10.12 42403* | Theorem *10.12 in [WhiteheadRussell] p. 146. In *10, this is treated as an axiom, and the proofs in *10 are based on this theorem. (Contributed by Andrew Salmon, 17-Jun-2011.) |
β’ (βπ₯(π β¨ π) β (π β¨ βπ₯π)) | ||
Theorem | pm10.14 42404 | Theorem *10.14 in [WhiteheadRussell] p. 146. (Contributed by Andrew Salmon, 17-Jun-2011.) |
β’ ((βπ₯π β§ βπ₯π) β ([π¦ / π₯]π β§ [π¦ / π₯]π)) | ||
Theorem | pm10.251 42405 | Theorem *10.251 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.) |
β’ (βπ₯ Β¬ π β Β¬ βπ₯π) | ||
Theorem | pm10.252 42406 | Theorem *10.252 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.) (New usage is discouraged.) |
β’ (Β¬ βπ₯π β βπ₯ Β¬ π) | ||
Theorem | pm10.253 42407 | Theorem *10.253 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.) |
β’ (Β¬ βπ₯π β βπ₯ Β¬ π) | ||
Theorem | albitr 42408 | Theorem *10.301 in [WhiteheadRussell] p. 151. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ ((βπ₯(π β π) β§ βπ₯(π β π)) β βπ₯(π β π)) | ||
Theorem | pm10.42 42409 | Theorem *10.42 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 17-Jun-2011.) |
β’ ((βπ₯π β¨ βπ₯π) β βπ₯(π β¨ π)) | ||
Theorem | pm10.52 42410* | Theorem *10.52 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯π β (βπ₯(π β π) β π)) | ||
Theorem | pm10.53 42411 | Theorem *10.53 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (Β¬ βπ₯π β βπ₯(π β π)) | ||
Theorem | pm10.541 42412* | Theorem *10.541 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯(π β (π β¨ π)) β (π β¨ βπ₯(π β π))) | ||
Theorem | pm10.542 42413* | Theorem *10.542 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯(π β (π β π)) β (π β βπ₯(π β π))) | ||
Theorem | pm10.55 42414 | Theorem *10.55 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ ((βπ₯(π β§ π) β§ βπ₯(π β π)) β (βπ₯π β§ βπ₯(π β π))) | ||
Theorem | pm10.56 42415 | Theorem *10.56 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ ((βπ₯(π β π) β§ βπ₯(π β§ π)) β βπ₯(π β§ π)) | ||
Theorem | pm10.57 42416 | Theorem *10.57 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯(π β (π β¨ π)) β (βπ₯(π β π) β¨ βπ₯(π β§ π))) | ||
Theorem | 2alanimi 42417 | Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ ((π β§ π) β π) β β’ ((βπ₯βπ¦π β§ βπ₯βπ¦π) β βπ₯βπ¦π) | ||
Theorem | 2al2imi 42418 | Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (π β (π β π)) β β’ (βπ₯βπ¦π β (βπ₯βπ¦π β βπ₯βπ¦π)) | ||
Theorem | pm11.11 42419 | Theorem *11.11 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.) |
β’ π β β’ βπ§βπ€[π§ / π₯][π€ / π¦]π | ||
Theorem | pm11.12 42420* | Theorem *11.12 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.) |
β’ (βπ₯βπ¦(π β¨ π) β (π β¨ βπ₯βπ¦π)) | ||
Theorem | 19.21vv 42421* | Compare Theorem *11.3 in [WhiteheadRussell] p. 161. Special case of theorem 19.21 of [Margaris] p. 90 with two quantifiers. See 19.21v 1943. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β π) β (π β βπ₯βπ¦π)) | ||
Theorem | 2alim 42422 | Theorem *11.32 in [WhiteheadRussell] p. 162. Theorem 19.20 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β π) β (βπ₯βπ¦π β βπ₯βπ¦π)) | ||
Theorem | 2albi 42423 | Theorem *11.33 in [WhiteheadRussell] p. 162. Theorem 19.15 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β π) β (βπ₯βπ¦π β βπ₯βπ¦π)) | ||
Theorem | 2exim 42424 | Theorem *11.34 in [WhiteheadRussell] p. 162. Theorem 19.22 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β π) β (βπ₯βπ¦π β βπ₯βπ¦π)) | ||
Theorem | 2exbi 42425 | Theorem *11.341 in [WhiteheadRussell] p. 162. Theorem 19.18 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β π) β (βπ₯βπ¦π β βπ₯βπ¦π)) | ||
Theorem | spsbce-2 42426 | Theorem *11.36 in [WhiteheadRussell] p. 162. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ ([π§ / π₯][π€ / π¦]π β βπ₯βπ¦π) | ||
Theorem | 19.33-2 42427 | Theorem *11.421 in [WhiteheadRussell] p. 163. Theorem 19.33 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ ((βπ₯βπ¦π β¨ βπ₯βπ¦π) β βπ₯βπ¦(π β¨ π)) | ||
Theorem | 19.36vv 42428* | Theorem *11.43 in [WhiteheadRussell] p. 163. Theorem 19.36 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 25-May-2011.) |
β’ (βπ₯βπ¦(π β π) β (βπ₯βπ¦π β π)) | ||
Theorem | 19.31vv 42429* | Theorem *11.44 in [WhiteheadRussell] p. 163. Theorem 19.31 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β¨ π) β (βπ₯βπ¦π β¨ π)) | ||
Theorem | 19.37vv 42430* | Theorem *11.46 in [WhiteheadRussell] p. 164. Theorem 19.37 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β π) β (π β βπ₯βπ¦π)) | ||
Theorem | 19.28vv 42431* | Theorem *11.47 in [WhiteheadRussell] p. 164. Theorem 19.28 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β§ π) β (π β§ βπ₯βπ¦π)) | ||
Theorem | pm11.52 42432 | Theorem *11.52 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β§ π) β Β¬ βπ₯βπ¦(π β Β¬ π)) | ||
Theorem | aaanv 42433* | Theorem *11.56 in [WhiteheadRussell] p. 165. Special case of aaan 2329. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ ((βπ₯π β§ βπ¦π) β βπ₯βπ¦(π β§ π)) | ||
Theorem | pm11.57 42434* | Theorem *11.57 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯π β βπ₯βπ¦(π β§ [π¦ / π₯]π)) | ||
Theorem | pm11.58 42435* | Theorem *11.58 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯π β βπ₯βπ¦(π β§ [π¦ / π₯]π)) | ||
Theorem | pm11.59 42436* | Theorem *11.59 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.) |
β’ (βπ₯(π β π) β βπ¦βπ₯((π β§ [π¦ / π₯]π) β (π β§ [π¦ / π₯]π))) | ||
Theorem | pm11.6 42437* | Theorem *11.6 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.) |
β’ (βπ₯(βπ¦(π β§ π) β§ π) β βπ¦(βπ₯(π β§ π) β§ π)) | ||
Theorem | pm11.61 42438* | Theorem *11.61 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ¦βπ₯(π β π) β βπ₯(π β βπ¦π)) | ||
Theorem | pm11.62 42439* | Theorem *11.62 in [WhiteheadRussell] p. 166. Importation combined with the rearrangement with quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦((π β§ π) β π) β βπ₯(π β βπ¦(π β π))) | ||
Theorem | pm11.63 42440 | Theorem *11.63 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (Β¬ βπ₯βπ¦π β βπ₯βπ¦(π β π)) | ||
Theorem | pm11.7 42441 | Theorem *11.7 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ (βπ₯βπ¦(π β¨ π) β βπ₯βπ¦π) | ||
Theorem | pm11.71 42442* | Theorem *11.71 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.) |
β’ ((βπ₯π β§ βπ¦π) β ((βπ₯(π β π) β§ βπ¦(π β π)) β βπ₯βπ¦((π β§ π) β (π β§ π)))) | ||
Theorem | sbeqal1 42443* | If π₯ = π¦ always implies π₯ = π§, then π¦ = π§. (Contributed by Andrew Salmon, 2-Jun-2011.) |
β’ (βπ₯(π₯ = π¦ β π₯ = π§) β π¦ = π§) | ||
Theorem | sbeqal1i 42444* | Suppose you know π₯ = π¦ implies π₯ = π§, assuming π₯ and π§ are distinct. Then, π¦ = π§. (Contributed by Andrew Salmon, 3-Jun-2011.) |
β’ (π₯ = π¦ β π₯ = π§) β β’ π¦ = π§ | ||
Theorem | sbeqal2i 42445* | If π₯ = π¦ implies π₯ = π§, then we can infer π§ = π¦. (Contributed by Andrew Salmon, 3-Jun-2011.) |
β’ (π₯ = π¦ β π₯ = π§) β β’ π§ = π¦ | ||
Theorem | axc5c4c711 42446 | Proof of a theorem that can act as a sole axiom for pure predicate calculus with ax-gen 1798 as the inference rule. This proof extends the idea of axc5c711 37276 and related theorems. (Contributed by Andrew Salmon, 14-Jul-2011.) |
β’ ((βπ₯βπ¦ Β¬ βπ₯βπ¦(βπ¦π β π) β (π β βπ¦(βπ¦π β π))) β (βπ¦π β βπ¦π)) | ||
Theorem | axc5c4c711toc5 42447 | Rederivation of sp 2177 from axc5c4c711 42446. Note that ax6 2384 is used for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) Revised to use ax6v 1973 instead of ax6 2384, so that this rederivation requires only ax6v 1973 and propositional calculus. (Revised by BJ, 14-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (βπ₯π β π) | ||
Theorem | axc5c4c711toc4 42448 | Rederivation of axc4 2316 from axc5c4c711 42446. Note that only propositional calculus is required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (βπ₯(βπ₯π β π) β (βπ₯π β βπ₯π)) | ||
Theorem | axc5c4c711toc7 42449 | Rederivation of axc7 2312 from axc5c4c711 42446. Note that neither axc7 2312 nor ax-11 2155 are required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ Β¬ βπ₯π β π) | ||
Theorem | axc5c4c711to11 42450 | Rederivation of ax-11 2155 from axc5c4c711 42446. Note that ax-11 2155 is not required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (βπ₯βπ¦π β βπ¦βπ₯π) | ||
Theorem | axc11next 42451* | This theorem shows that, given axextb 2712, we can derive a version of axc11n 2426. However, it is weaker than axc11n 2426 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 16-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (βπ₯ π₯ = π§ β βπ§ π§ = π₯) | ||
Theorem | pm13.13a 42452 | One result of theorem *13.13 in [WhiteheadRussell] p. 178. A note on the section - to make the theorems more usable, and because inequality is notation for set theory (it is not defined in the predicate calculus section), this section will use classes instead of sets. (Contributed by Andrew Salmon, 3-Jun-2011.) |
β’ ((π β§ π₯ = π΄) β [π΄ / π₯]π) | ||
Theorem | pm13.13b 42453 | Theorem *13.13 in [WhiteheadRussell] p. 178 with different variable substitution. (Contributed by Andrew Salmon, 3-Jun-2011.) |
β’ (([π΄ / π₯]π β§ π₯ = π΄) β π) | ||
Theorem | pm13.14 42454 | Theorem *13.14 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.) |
β’ (([π΄ / π₯]π β§ Β¬ π) β π₯ β π΄) | ||
Theorem | pm13.192 42455* | Theorem *13.192 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.) |
β’ (βπ¦(βπ₯(π₯ = π΄ β π₯ = π¦) β§ π) β [π΄ / π¦]π) | ||
Theorem | pm13.193 42456 | Theorem *13.193 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) |
β’ ((π β§ π₯ = π¦) β ([π¦ / π₯]π β§ π₯ = π¦)) | ||
Theorem | pm13.194 42457 | Theorem *13.194 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) |
β’ ((π β§ π₯ = π¦) β ([π¦ / π₯]π β§ π β§ π₯ = π¦)) | ||
Theorem | pm13.195 42458* | Theorem *13.195 in [WhiteheadRussell] p. 179. This theorem is very similar to sbc5 3766. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.) |
β’ (βπ¦(π¦ = π΄ β§ π) β [π΄ / π¦]π) | ||
Theorem | pm13.196a 42459* | Theorem *13.196 in [WhiteheadRussell] p. 179. The only difference is the position of the substituted variable. (Contributed by Andrew Salmon, 3-Jun-2011.) |
β’ (Β¬ π β βπ¦([π¦ / π₯]π β π¦ β π₯)) | ||
Theorem | 2sbc6g 42460* | Theorem *13.21 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) |
β’ ((π΄ β πΆ β§ π΅ β π·) β (βπ§βπ€((π§ = π΄ β§ π€ = π΅) β π) β [π΄ / π§][π΅ / π€]π)) | ||
Theorem | 2sbc5g 42461* | Theorem *13.22 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) |
β’ ((π΄ β πΆ β§ π΅ β π·) β (βπ§βπ€((π§ = π΄ β§ π€ = π΅) β§ π) β [π΄ / π§][π΅ / π€]π)) | ||
Theorem | iotain 42462 | Equivalence between two different forms of β©. (Contributed by Andrew Salmon, 15-Jul-2011.) |
β’ (β!π₯π β β© {π₯ β£ π} = (β©π₯π)) | ||
Theorem | iotaexeu 42463 | The iota class exists. This theorem does not require ax-nul 5262 for its proof. (Contributed by Andrew Salmon, 11-Jul-2011.) |
β’ (β!π₯π β (β©π₯π) β V) | ||
Theorem | iotasbc 42464* | Definition *14.01 in [WhiteheadRussell] p. 184. In Principia Mathematica, Russell and Whitehead define β© in terms of a function of (β©π₯π). Their definition differs in that a function of (β©π₯π) evaluates to "false" when there isn't a single π₯ that satisfies π. (Contributed by Andrew Salmon, 11-Jul-2011.) |
β’ (β!π₯π β ([(β©π₯π) / π¦]π β βπ¦(βπ₯(π β π₯ = π¦) β§ π))) | ||
Theorem | iotasbc2 42465* | Theorem *14.111 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.) |
β’ ((β!π₯π β§ β!π₯π) β ([(β©π₯π) / π¦][(β©π₯π) / π§]π β βπ¦βπ§(βπ₯(π β π₯ = π¦) β§ βπ₯(π β π₯ = π§) β§ π))) | ||
Theorem | pm14.12 42466* | Theorem *14.12 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.) |
β’ (β!π₯π β βπ₯βπ¦((π β§ [π¦ / π₯]π) β π₯ = π¦)) | ||
Theorem | pm14.122a 42467* | Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
β’ (π΄ β π β (βπ₯(π β π₯ = π΄) β (βπ₯(π β π₯ = π΄) β§ [π΄ / π₯]π))) | ||
Theorem | pm14.122b 42468* | Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
β’ (π΄ β π β ((βπ₯(π β π₯ = π΄) β§ [π΄ / π₯]π) β (βπ₯(π β π₯ = π΄) β§ βπ₯π))) | ||
Theorem | pm14.122c 42469* | Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
β’ (π΄ β π β (βπ₯(π β π₯ = π΄) β (βπ₯(π β π₯ = π΄) β§ βπ₯π))) | ||
Theorem | pm14.123a 42470* | Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
β’ ((π΄ β π β§ π΅ β π) β (βπ§βπ€(π β (π§ = π΄ β§ π€ = π΅)) β (βπ§βπ€(π β (π§ = π΄ β§ π€ = π΅)) β§ [π΄ / π§][π΅ / π€]π))) | ||
Theorem | pm14.123b 42471* | Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
β’ ((π΄ β π β§ π΅ β π) β ((βπ§βπ€(π β (π§ = π΄ β§ π€ = π΅)) β§ [π΄ / π§][π΅ / π€]π) β (βπ§βπ€(π β (π§ = π΄ β§ π€ = π΅)) β§ βπ§βπ€π))) | ||
Theorem | pm14.123c 42472* | Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
β’ ((π΄ β π β§ π΅ β π) β (βπ§βπ€(π β (π§ = π΄ β§ π€ = π΅)) β (βπ§βπ€(π β (π§ = π΄ β§ π€ = π΅)) β§ βπ§βπ€π))) | ||
Theorem | pm14.18 42473 | Theorem *14.18 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.) |
β’ (β!π₯π β (βπ₯π β [(β©π₯π) / π₯]π)) | ||
Theorem | iotaequ 42474* | Theorem *14.2 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.) |
β’ (β©π₯π₯ = π¦) = π¦ | ||
Theorem | iotavalb 42475* | Theorem *14.202 in [WhiteheadRussell] p. 189. A biconditional version of iotaval 6463. (Contributed by Andrew Salmon, 11-Jul-2011.) |
β’ (β!π₯π β (βπ₯(π β π₯ = π¦) β (β©π₯π) = π¦)) | ||
Theorem | iotasbc5 42476* | Theorem *14.205 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 11-Jul-2011.) |
β’ (β!π₯π β ([(β©π₯π) / π¦]π β βπ¦(π¦ = (β©π₯π) β§ π))) | ||
Theorem | pm14.24 42477* | Theorem *14.24 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.) |
β’ (β!π₯π β βπ¦([π¦ / π₯]π β π¦ = (β©π₯π))) | ||
Theorem | iotavalsb 42478* | Theorem *14.242 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.) |
β’ (βπ₯(π β π₯ = π¦) β ([π¦ / π§]π β [(β©π₯π) / π§]π)) | ||
Theorem | sbiota1 42479 | Theorem *14.25 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.) |
β’ (β!π₯π β (βπ₯(π β π) β [(β©π₯π) / π₯]π)) | ||
Theorem | sbaniota 42480 | Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.) |
β’ (β!π₯π β (βπ₯(π β§ π) β [(β©π₯π) / π₯]π)) | ||
Theorem | eubiOLD 42481 | Obsolete proof of eubi 2584 as of 7-Oct-2022. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (βπ₯(π β π) β (β!π₯π β β!π₯π)) | ||
Theorem | iotasbcq 42482 | Theorem *14.272 in [WhiteheadRussell] p. 193. (Contributed by Andrew Salmon, 11-Jul-2011.) |
β’ (βπ₯(π β π) β ([(β©π₯π) / π¦]π β [(β©π₯π) / π¦]π)) | ||
Theorem | elnev 42483* | Any set that contains one element less than the universe is not equal to it. (Contributed by Andrew Salmon, 16-Jun-2011.) |
β’ (π΄ β V β {π₯ β£ Β¬ π₯ = π΄} β V) | ||
Theorem | rusbcALT 42484 | A version of Russell's paradox which is proven using proper substitution. (Contributed by Andrew Salmon, 18-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ {π₯ β£ π₯ β π₯} β V | ||
Theorem | compeq 42485* | Equality between two ways of saying "the complement of π΄". (Contributed by Andrew Salmon, 15-Jul-2011.) |
β’ (V β π΄) = {π₯ β£ Β¬ π₯ β π΄} | ||
Theorem | compne 42486 | The complement of π΄ is not equal to π΄. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 11-Nov-2021.) |
β’ (V β π΄) β π΄ | ||
Theorem | compab 42487 | Two ways of saying "the complement of a class abstraction". (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
β’ (V β {π§ β£ π}) = {π§ β£ Β¬ π} | ||
Theorem | conss2 42488 | Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.) |
β’ (π΄ β (V β π΅) β π΅ β (V β π΄)) | ||
Theorem | conss1 42489 | Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.) |
β’ ((V β π΄) β π΅ β (V β π΅) β π΄) | ||
Theorem | ralbidar 42490 | More general form of ralbida 3252. (Contributed by Andrew Salmon, 25-Jul-2011.) |
β’ (π β βπ₯ β π΄ π) & β’ ((π β§ π₯ β π΄) β (π β π)) β β’ (π β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | rexbidar 42491 | More general form of rexbida 3254. (Contributed by Andrew Salmon, 25-Jul-2011.) |
β’ (π β βπ₯ β π΄ π) & β’ ((π β§ π₯ β π΄) β (π β π)) β β’ (π β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | dropab1 42492 | Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.) |
β’ (βπ₯ π₯ = π¦ β {β¨π₯, π§β© β£ π} = {β¨π¦, π§β© β£ π}) | ||
Theorem | dropab2 42493 | Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.) |
β’ (βπ₯ π₯ = π¦ β {β¨π§, π₯β© β£ π} = {β¨π§, π¦β© β£ π}) | ||
Theorem | ipo0 42494 | If the identity relation partially orders any class, then that class is the null class. (Contributed by Andrew Salmon, 25-Jul-2011.) |
β’ ( I Po π΄ β π΄ = β ) | ||
Theorem | ifr0 42495 | A class that is founded by the identity relation is null. (Contributed by Andrew Salmon, 25-Jul-2011.) |
β’ ( I Fr π΄ β π΄ = β ) | ||
Theorem | ordpss 42496 | ordelpss 6342 with an antecedent removed. (Contributed by Andrew Salmon, 25-Jul-2011.) |
β’ (Ord π΅ β (π΄ β π΅ β π΄ β π΅)) | ||
Theorem | fvsb 42497* | Explicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.) |
β’ (β!π¦ π΄πΉπ¦ β ([(πΉβπ΄) / π₯]π β βπ₯(βπ¦(π΄πΉπ¦ β π¦ = π₯) β§ π))) | ||
Theorem | fveqsb 42498* | Implicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.) |
β’ (π₯ = (πΉβπ΄) β (π β π)) & β’ β²π₯π β β’ (β!π¦ π΄πΉπ¦ β (π β βπ₯(βπ¦(π΄πΉπ¦ β π¦ = π₯) β§ π))) | ||
Theorem | xpexb 42499 | A Cartesian product exists iff its converse does. Corollary 6.9(1) in [TakeutiZaring] p. 26. (Contributed by Andrew Salmon, 13-Nov-2011.) |
β’ ((π΄ Γ π΅) β V β (π΅ Γ π΄) β V) | ||
Theorem | trelpss 42500 | An element of a transitive set is a proper subset of it. Theorem 7.2 in [TakeutiZaring] p. 35. Unlike tz7.2 5615, ax-reg 9462 is required for its proof. (Contributed by Andrew Salmon, 13-Nov-2011.) |
β’ ((Tr π΄ β§ π΅ β π΄) β π΅ β π΄) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |