Home | Metamath
Proof Explorer Theorem List (p. 387 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sbeqalbi 38601* | When both and and and are both distinct, then the converse of sbeqal1 holds as well. (Contributed by Andrew Salmon, 2-Jun-2011.) |
Theorem | axc5c4c711 38602 | Proof of a theorem that can act as a sole axiom for pure predicate calculus with ax-gen 1722 as the inference rule. This proof extends the idea of axc5c711 34203 and related theorems. (Contributed by Andrew Salmon, 14-Jul-2011.) |
Theorem | axc5c4c711toc5 38603 | Rederivation of sp 2053 from axc5c4c711 38602. Note that ax6 2251 is used for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) Revised to use ax6v 1889 instead of ax6 2251, so that this rederivation requires only ax6v 1889 and propositional calculus. (Revised by BJ, 14-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc5c4c711toc4 38604 | Rederivation of axc4 2130 from axc5c4c711 38602. 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 38605 | Rederivation of axc7 2132 from axc5c4c711 38602. Note that neither axc7 2132 nor ax-11 2034 are required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc5c4c711to11 38606 | Rederivation of ax-11 2034 from axc5c4c711 38602. Note that ax-11 2034 is not required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc11next 38607* | This theorem shows that, given axext4 2606, we can derive a version of axc11n 2307. However, it is weaker than axc11n 2307 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 38608 | 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 38609 | Theorem *13.13 in [WhiteheadRussell] p. 178 with different variable substitution. (Contributed by Andrew Salmon, 3-Jun-2011.) |
Theorem | pm13.14 38610 | Theorem *13.14 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.) |
Theorem | pm13.192 38611* | Theorem *13.192 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.) |
Theorem | pm13.193 38612 | Theorem *13.193 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) |
Theorem | pm13.194 38613 | Theorem *13.194 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) |
Theorem | pm13.195 38614* | Theorem *13.195 in [WhiteheadRussell] p. 179. This theorem is very similar to sbc5 3460. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.) |
Theorem | pm13.196a 38615* | 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 38616* | Theorem *13.21 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) |
Theorem | 2sbc5g 38617* | Theorem *13.22 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) |
Theorem | iotain 38618 | Equivalence between two different forms of . (Contributed by Andrew Salmon, 15-Jul-2011.) |
Theorem | iotaexeu 38619 | The iota class exists. This theorem does not require ax-nul 4789 for its proof. (Contributed by Andrew Salmon, 11-Jul-2011.) |
Theorem | iotasbc 38620* | 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 38621* | Theorem *14.111 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.) |
Theorem | pm14.12 38622* | Theorem *14.12 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.) |
Theorem | pm14.122a 38623* | Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
Theorem | pm14.122b 38624* | Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
Theorem | pm14.122c 38625* | Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
Theorem | pm14.123a 38626* | Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
Theorem | pm14.123b 38627* | Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
Theorem | pm14.123c 38628* | Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
Theorem | pm14.18 38629 | Theorem *14.18 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.) |
Theorem | iotaequ 38630* | Theorem *14.2 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.) |
Theorem | iotavalb 38631* | Theorem *14.202 in [WhiteheadRussell] p. 189. A biconditional version of iotaval 5862. (Contributed by Andrew Salmon, 11-Jul-2011.) |
Theorem | iotasbc5 38632* | Theorem *14.205 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 11-Jul-2011.) |
Theorem | pm14.24 38633* | Theorem *14.24 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.) |
Theorem | iotavalsb 38634* | Theorem *14.242 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.) |
Theorem | sbiota1 38635 | Theorem *14.25 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.) |
Theorem | sbaniota 38636 | Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.) |
Theorem | eubi 38637 | Theorem *14.271 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.) |
Theorem | iotasbcq 38638 | Theorem *14.272 in [WhiteheadRussell] p. 193. (Contributed by Andrew Salmon, 11-Jul-2011.) |
Theorem | elnev 38639* | Any set that contains one element less than the universe is not equal to it. (Contributed by Andrew Salmon, 16-Jun-2011.) |
Theorem | rusbcALT 38640 | 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.) |
Theorem | compel 38641 | Equivalence between two ways of saying "is a member of the complement of ." (Contributed by Andrew Salmon, 15-Jul-2011.) |
Theorem | compeq 38642* | Equality between two ways of saying "the complement of ." (Contributed by Andrew Salmon, 15-Jul-2011.) |
Theorem | compne 38643 | The complement of is not equal to . (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 11-Nov-2021.) |
Theorem | compneOLD 38644 | Obsolete proof of compne 38643 as of 11-Nov-2021. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | compab 38645 | 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.) |
Theorem | conss34OLD 38646 | Obsolete proof of complss 3751 as of 7-Aug-2021. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | conss2 38647 | Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.) |
Theorem | conss1 38648 | Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.) |
Theorem | ralbidar 38649 | More general form of ralbida 2982. (Contributed by Andrew Salmon, 25-Jul-2011.) |
Theorem | rexbidar 38650 | More general form of rexbida 3047. (Contributed by Andrew Salmon, 25-Jul-2011.) |
Theorem | dropab1 38651 | Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.) |
Theorem | dropab2 38652 | Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.) |
Theorem | ipo0 38653 | If the identity relation partially orders any class, then that class is the null class. (Contributed by Andrew Salmon, 25-Jul-2011.) |
Theorem | ifr0 38654 | A class that is founded by the identity relation is null. (Contributed by Andrew Salmon, 25-Jul-2011.) |
Theorem | ordpss 38655 | ordelpss 5751 with an antecedent removed. (Contributed by Andrew Salmon, 25-Jul-2011.) |
Theorem | fvsb 38656* | Explicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.) |
Theorem | fveqsb 38657* | Implicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.) |
Theorem | xpexb 38658 | A Cartesian product exists iff its converse does. Corollary 6.9(1) in [TakeutiZaring] p. 26. (Contributed by Andrew Salmon, 13-Nov-2011.) |
Theorem | trelpss 38659 | An element of a transitive set is a proper subset of it. Theorem 7.2 in [TakeutiZaring] p. 35. Unlike tz7.2 5098, ax-reg 8497 is required for its proof. (Contributed by Andrew Salmon, 13-Nov-2011.) |
Theorem | addcomgi 38660 | Generalization of commutative law for addition. Simplifies proofs dealing with vectors. However, it is dependent on our particular definition of ordered pair. (Contributed by Andrew Salmon, 28-Jan-2012.) (Revised by Mario Carneiro, 6-May-2015.) |
Syntax | cplusr 38661 | Introduce the operation of vector addition. |
Syntax | cminusr 38662 | Introduce the operation of vector subtraction. |
Syntax | ctimesr 38663 | Introduce the operation of scalar multiplication. |
Syntax | cptdfc 38664 | is a predicate that is crucial for the definition of lines as well as proving a number of important theorems. |
Syntax | crr3c 38665 | is a class. |
Syntax | cline3 38666 | is a class. |
Definition | df-addr 38667* | Define the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.) |
Definition | df-subr 38668* | Define the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.) |
Definition | df-mulv 38669* | Define the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.) |
Theorem | addrval 38670* | Value of the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.) |
Theorem | subrval 38671* | Value of the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.) |
Theorem | mulvval 38672* | Value of the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.) |
Theorem | addrfv 38673 | Vector addition at a value. The operation takes each vector and and forms a new vector whose values are the sum of each of the values of and . (Contributed by Andrew Salmon, 27-Jan-2012.) |
Theorem | subrfv 38674 | Vector subtraction at a value. (Contributed by Andrew Salmon, 27-Jan-2012.) |
Theorem | mulvfv 38675 | Scalar multiplication at a value. (Contributed by Andrew Salmon, 27-Jan-2012.) |
Theorem | addrfn 38676 | Vector addition produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.) |
Theorem | subrfn 38677 | Vector subtraction produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.) |
Theorem | mulvfn 38678 | Scalar multiplication producees a function. (Contributed by Andrew Salmon, 27-Jan-2012.) |
Theorem | addrcom 38679 | Vector addition is commutative. (Contributed by Andrew Salmon, 28-Jan-2012.) |
Definition | df-ptdf 38680* | Define the predicate , which is a utility definition used to shorten definitions and simplify proofs. (Contributed by Andrew Salmon, 15-Jul-2012.) |
Definition | df-rr3 38681 | Define the set of all points . We define each point as a function to allow the use of vector addition and subtraction as well as scalar multiplication in our proofs. (Contributed by Andrew Salmon, 15-Jul-2012.) |
Definition | df-line3 38682* | Define the set of all lines. A line is an infinite subset of that satisfies a property. (Contributed by Andrew Salmon, 15-Jul-2012.) |
We are sad to report the passing of long-time contributor Alan Sare (Nov. 9, 1954 - Mar. 23, 2019). Alan's first contribution to Metamath was a shorter proof for tfrlem8 7480 in 2008. He developed a tool called "completeusersproof" that assists developing proofs using his "virtual deduction" method: http://us.metamath.org/other.html#completeusersproof. His virtual deduction method is explained in the comment for wvd1 38785. Below are some excerpts from his first emails to NM in 2007: ...I have been interested in proving set theory theorems for many years for mental exercise. I enjoy it. I have used a book by Martin Zuckerman. It is informal. I am interested in completely and perfectly proving theorems. Mr. Zuckerman leaves out most of the steps of a proof, of course, like most authors do, as you have noted. A complete proof for higher theorems would require a volume of writing similar to the metamath documents. So I am frustrated when I am not capable of constructing a proof and Zuckerman leaves out steps I do not understand. I could search for the steps in other texts, but I don't do that too much. Metamath may be the answer for me.... ...If we go beyond mathematics, I believe that it is possible to write down all human knowledge in a way similar to the way you have explicated large areas of mathematics. Of course, that would be a much, much more difficult job. For example, it is possible to take a hard science like physics, construct axioms based on experimental results, and to cast all of physics into a collection of axioms and theorems. Maybe this has already been attempted, although I am not familiar with it. When one then moves on to the soft sciences such as social science, this job gets much more difficult. The key is: All human thought consists of logical operations on abstract objects. Usually, these logical operations are done informally. There is no reason why one cannot take any subject and explicate it and take it down to the indivisible postulates in a formal rigorous way.... ...When I read a math book or an engineering book I come across something I don't understand and I am compelled to understand it. But, often it is hopeless. I don't have the time. Or, I would have to read the same thing by multiple authors in the hope that different authors would give parts of the working proof that others have omitted. It is very inefficient. Because I have always been inclined to "get to the bottom" for a 100% fully understood proof.... | ||
Theorem | idiALT 38683 | Placeholder for idi 2. Though unnecessary, this theorem is sometimes used in proofs in this mathbox for pedagogical purposes. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | exbir 38684 | Exportation implication also converting the consequent from a biconditional to an implication. Derived automatically from exbirVD 39088. (Contributed by Alan Sare, 31-Dec-2011.) |
Theorem | 3impexpbicom 38685 | Version of 3impexp 1289 where in addition the consequent is commuted. (Contributed by Alan Sare, 31-Dec-2011.) |
Theorem | 3impexpbicomi 38686 | Inference associated with 3impexpbicom 38685. Derived automatically from 3impexpbicomiVD 39093. (Contributed by Alan Sare, 31-Dec-2011.) |
Theorem | bi1imp 38687 | Importation inference similar to imp 445, except the outermost implication of the hypothesis is a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
Theorem | bi2imp 38688 | Importation inference similar to imp 445, except both implications of the hypothesis are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) |
Theorem | bi3impb 38689 | Similar to 3impb 1260 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
Theorem | bi3impa 38690 | Similar to 3impa 1259 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
Theorem | bi23impib 38691 | 3impib 1262 with the inner implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
Theorem | bi13impib 38692 | 3impib 1262 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
Theorem | bi123impib 38693 | 3impib 1262 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) |
Theorem | bi13impia 38694 | 3impia 1261 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
Theorem | bi123impia 38695 | 3impia 1261 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) |
Theorem | bi33imp12 38696 | 3imp 1256 with innermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
Theorem | bi23imp13 38697 | 3imp 1256 with middle implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
Theorem | bi13imp23 38698 | 3imp 1256 with outermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
Theorem | bi13imp2 38699 | Similar to 3imp 1256 except the outermost and innermost implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) |
Theorem | bi12imp3 38700 | Similar to 3imp 1256 except all but innermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |