Home | Intuitionistic Logic Explorer Theorem List (p. 29 of 133) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rspc2gv 2801* | Restricted specialization with two quantifiers, using implicit substitution. (Contributed by BJ, 2-Dec-2021.) |
Theorem | rspc2v 2802* | 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.) |
Theorem | rspc2va 2803* | 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014.) |
Theorem | rspc2ev 2804* | 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.) |
Theorem | rspc3v 2805* | 3-variable restricted specialization, using implicit substitution. (Contributed by NM, 10-May-2005.) |
Theorem | rspc3ev 2806* | 3-variable restricted existentional specialization, using implicit substitution. (Contributed by NM, 25-Jul-2012.) |
Theorem | rspceeqv 2807* | Restricted existential specialization in an equality, using implicit substitution. (Contributed by BJ, 2-Sep-2022.) |
Theorem | eqvinc 2808* | A variable introduction law for class equality. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | eqvincg 2809* | A variable introduction law for class equality, deduction version. (Contributed by Thierry Arnoux, 2-Mar-2017.) |
Theorem | eqvincf 2810 | A variable introduction law for class equality, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 14-Sep-2003.) |
Theorem | alexeq 2811* | Two ways to express substitution of for in . (Contributed by NM, 2-Mar-1995.) |
Theorem | ceqex 2812* | Equality implies equivalence with substitution. (Contributed by NM, 2-Mar-1995.) |
Theorem | ceqsexg 2813* | A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 11-Oct-2004.) |
Theorem | ceqsexgv 2814* | Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 29-Dec-1996.) |
Theorem | ceqsrexv 2815* | Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 30-Apr-2004.) |
Theorem | ceqsrexbv 2816* | Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by Mario Carneiro, 14-Mar-2014.) |
Theorem | ceqsrex2v 2817* | Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 29-Oct-2005.) |
Theorem | clel2 2818* | An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.) |
Theorem | clel3g 2819* | An alternate definition of class membership when the class is a set. (Contributed by NM, 13-Aug-2005.) |
Theorem | clel3 2820* | An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.) |
Theorem | clel4 2821* | An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.) |
Theorem | pm13.183 2822* | Compare theorem *13.183 in [WhiteheadRussell] p. 178. Only is required to be a set. (Contributed by Andrew Salmon, 3-Jun-2011.) |
Theorem | rr19.3v 2823* | Restricted quantifier version of Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 25-Oct-2012.) |
Theorem | rr19.28v 2824* | Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 29-Oct-2012.) |
Theorem | elabgt 2825* | Membership in a class abstraction, using implicit substitution. (Closed theorem version of elabg 2830.) (Contributed by NM, 7-Nov-2005.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | elabgf 2826 | Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.) (Revised by Mario Carneiro, 12-Oct-2016.) |
Theorem | elabf 2827* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 1-Aug-1994.) (Revised by Mario Carneiro, 12-Oct-2016.) |
Theorem | elab 2828* | Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 1-Aug-1994.) |
Theorem | elabd 2829* | Explicit demonstration the class is not empty by the example . (Contributed by RP, 12-Aug-2020.) |
Theorem | elabg 2830* | Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 14-Apr-1995.) |
Theorem | elab2g 2831* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.) |
Theorem | elab2 2832* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.) |
Theorem | elab4g 2833* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 17-Oct-2012.) |
Theorem | elab3gf 2834 | Membership in a class abstraction, with a weaker antecedent than elabgf 2826. (Contributed by NM, 6-Sep-2011.) |
Theorem | elab3g 2835* | Membership in a class abstraction, with a weaker antecedent than elabg 2830. (Contributed by NM, 29-Aug-2006.) |
Theorem | elab3 2836* | Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000.) |
Theorem | elrabi 2837* | Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.) |
Theorem | elrabf 2838 | Membership in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.) |
Theorem | elrab3t 2839* | Membership in a restricted class abstraction, using implicit substitution. (Closed theorem version of elrab3 2841.) (Contributed by Thierry Arnoux, 31-Aug-2017.) |
Theorem | elrab 2840* | Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.) |
Theorem | elrab3 2841* | Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 5-Oct-2006.) |
Theorem | elrabd 2842* | Membership in a restricted class abstraction, using implicit substitution. Deduction version of elrab 2840. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
Theorem | elrab2 2843* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.) |
Theorem | ralab 2844* | Universal quantification over a class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | ralrab 2845* | Universal quantification over a restricted class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | rexab 2846* | Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 23-Jan-2014.) (Revised by Mario Carneiro, 3-Sep-2015.) |
Theorem | rexrab 2847* | Existential quantification over a class abstraction. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Mario Carneiro, 3-Sep-2015.) |
Theorem | ralab2 2848* | Universal quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015.) |
Theorem | ralrab2 2849* | Universal quantification over a restricted class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015.) |
Theorem | rexab2 2850* | Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015.) |
Theorem | rexrab2 2851* | Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015.) |
Theorem | abidnf 2852* | Identity used to create closed-form versions of bound-variable hypothesis builders for class expressions. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Mario Carneiro, 12-Oct-2016.) |
Theorem | dedhb 2853* | A deduction theorem for converting the inference => into a closed theorem. Use nfa1 1521 and nfab 2286 to eliminate the hypothesis of the substitution instance of the inference. For converting the inference form into a deduction form, abidnf 2852 is useful. (Contributed by NM, 8-Dec-2006.) |
Theorem | eqeu 2854* | A condition which implies existential uniqueness. (Contributed by Jeff Hankins, 8-Sep-2009.) |
Theorem | eueq 2855* | Equality has existential uniqueness. (Contributed by NM, 25-Nov-1994.) |
Theorem | eueq1 2856* | Equality has existential uniqueness. (Contributed by NM, 5-Apr-1995.) |
Theorem | eueq2dc 2857* | Equality has existential uniqueness (split into 2 cases). (Contributed by NM, 5-Apr-1995.) |
DECID | ||
Theorem | eueq3dc 2858* | Equality has existential uniqueness (split into 3 cases). (Contributed by NM, 5-Apr-1995.) (Proof shortened by Mario Carneiro, 28-Sep-2015.) |
DECID DECID | ||
Theorem | moeq 2859* | There is at most one set equal to a class. (Contributed by NM, 8-Mar-1995.) |
Theorem | moeq3dc 2860* | "At most one" property of equality (split into 3 cases). (Contributed by Jim Kingdon, 7-Jul-2018.) |
DECID DECID | ||
Theorem | mosubt 2861* | "At most one" remains true after substitution. (Contributed by Jim Kingdon, 18-Jan-2019.) |
Theorem | mosub 2862* | "At most one" remains true after substitution. (Contributed by NM, 9-Mar-1995.) |
Theorem | mo2icl 2863* | Theorem for inferring "at most one." (Contributed by NM, 17-Oct-1996.) |
Theorem | mob2 2864* | Consequence of "at most one." (Contributed by NM, 2-Jan-2015.) |
Theorem | moi2 2865* | Consequence of "at most one." (Contributed by NM, 29-Jun-2008.) |
Theorem | mob 2866* | Equality implied by "at most one." (Contributed by NM, 18-Feb-2006.) |
Theorem | moi 2867* | Equality implied by "at most one." (Contributed by NM, 18-Feb-2006.) |
Theorem | morex 2868* | Derive membership from uniqueness. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | euxfr2dc 2869* | Transfer existential uniqueness from a variable to another variable contained in expression . (Contributed by NM, 14-Nov-2004.) |
DECID | ||
Theorem | euxfrdc 2870* | Transfer existential uniqueness from a variable to another variable contained in expression . (Contributed by NM, 14-Nov-2004.) |
DECID | ||
Theorem | euind 2871* | Existential uniqueness via an indirect equality. (Contributed by NM, 11-Oct-2010.) |
Theorem | reu2 2872* | A way to express restricted uniqueness. (Contributed by NM, 22-Nov-1994.) |
Theorem | reu6 2873* | A way to express restricted uniqueness. (Contributed by NM, 20-Oct-2006.) |
Theorem | reu3 2874* | A way to express restricted uniqueness. (Contributed by NM, 24-Oct-2006.) |
Theorem | reu6i 2875* | A condition which implies existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.) |
Theorem | eqreu 2876* | A condition which implies existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.) |
Theorem | rmo4 2877* | Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by NM, 16-Jun-2017.) |
Theorem | reu4 2878* | Restricted uniqueness using implicit substitution. (Contributed by NM, 23-Nov-1994.) |
Theorem | reu7 2879* | Restricted uniqueness using implicit substitution. (Contributed by NM, 24-Oct-2006.) |
Theorem | reu8 2880* | Restricted uniqueness using implicit substitution. (Contributed by NM, 24-Oct-2006.) |
Theorem | rmo3f 2881* | Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.) |
Theorem | rmo4f 2882* | Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by Thierry Arnoux, 11-Oct-2016.) (Revised by Thierry Arnoux, 8-Mar-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.) |
Theorem | reueq 2883* | Equality has existential uniqueness. (Contributed by Mario Carneiro, 1-Sep-2015.) |
Theorem | rmoan 2884 | Restricted "at most one" still holds when a conjunct is added. (Contributed by NM, 16-Jun-2017.) |
Theorem | rmoim 2885 | Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
Theorem | rmoimia 2886 | Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
Theorem | rmoimi2 2887 | Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
Theorem | 2reuswapdc 2888* | A condition allowing swap of uniqueness and existential quantifiers. (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by NM, 16-Jun-2017.) |
DECID | ||
Theorem | reuind 2889* | Existential uniqueness via an indirect equality. (Contributed by NM, 16-Oct-2010.) |
Theorem | 2rmorex 2890* | Double restricted quantification with "at most one," analogous to 2moex 2085. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
Theorem | nelrdva 2891* | Deduce negative membership from an implication. (Contributed by Thierry Arnoux, 27-Nov-2017.) |
This is a very useless definition, which "abbreviates" as CondEq . What this display hides, though, is that the first expression, even though it has a shorter constant string, is actually much more complicated in its parse tree: it is parsed as (wi (wceq (cv vx) (cv vy)) wph), while the CondEq version is parsed as (wcdeq vx vy wph). It also allows us to give a name to the specific ternary operation . This is all used as part of a metatheorem: we want to say that and are provable, for any expressions or in the language. The proof is by induction, so the base case is each of the primitives, which is why you will see a theorem for each of the set.mm primitive operations. The metatheorem comes with a disjoint variables condition: every variable in is assumed disjoint from except itself. For such a proof by induction, we must consider each of the possible forms of . If it is a variable other than , then we have CondEq or CondEq , which is provable by cdeqth 2896 and reflexivity. Since we are only working with class and wff expressions, it can't be itself in set.mm, but if it was we'd have to also prove CondEq (where set equality is being used on the right). Otherwise, it is a primitive operation applied to smaller expressions. In these cases, for each setvar variable parameter to the operation, we must consider if it is equal to or not, which yields 2^n proof obligations. Luckily, all primitive operations in set.mm have either zero or one set variable, so we only need to prove one statement for the non-set constructors (like implication) and two for the constructors taking a set (the forall and the class builder). In each of the primitive proofs, we are allowed to assume that is disjoint from and vice versa, because this is maintained through the induction. This is how we satisfy the disjoint variable conditions of cdeqab1 2901 and cdeqab 2899. | ||
Syntax | wcdeq 2892 | Extend wff notation to include conditional equality. This is a technical device used in the proof that is the not-free predicate, and that definitions are conservative as a result. |
CondEq | ||
Definition | df-cdeq 2893 | Define conditional equality. All the notation to the left of the is fake; the parentheses and arrows are all part of the notation, which could equally well be written CondEq. On the right side is the actual implication arrow. The reason for this definition is to "flatten" the structure on the right side (whose tree structure is something like (wi (wceq (cv vx) (cv vy)) wph) ) into just (wcdeq vx vy wph). (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq | ||
Theorem | cdeqi 2894 | Deduce conditional equality. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq | ||
Theorem | cdeqri 2895 | Property of conditional equality. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq | ||
Theorem | cdeqth 2896 | Deduce conditional equality from a theorem. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq | ||
Theorem | cdeqnot 2897 | Distribute conditional equality over negation. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq CondEq | ||
Theorem | cdeqal 2898* | Distribute conditional equality over quantification. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq CondEq | ||
Theorem | cdeqab 2899* | Distribute conditional equality over abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq CondEq | ||
Theorem | cdeqal1 2900* | Distribute conditional equality over quantification. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq CondEq |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |