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 | rspc3ev 2801* | 3-variable restricted existentional specialization, using implicit substitution. (Contributed by NM, 25-Jul-2012.) |
Theorem | rspceeqv 2802* | Restricted existential specialization in an equality, using implicit substitution. (Contributed by BJ, 2-Sep-2022.) |
Theorem | eqvinc 2803* | A variable introduction law for class equality. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | eqvincg 2804* | A variable introduction law for class equality, deduction version. (Contributed by Thierry Arnoux, 2-Mar-2017.) |
Theorem | eqvincf 2805 | A variable introduction law for class equality, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 14-Sep-2003.) |
Theorem | alexeq 2806* | Two ways to express substitution of for in . (Contributed by NM, 2-Mar-1995.) |
Theorem | ceqex 2807* | Equality implies equivalence with substitution. (Contributed by NM, 2-Mar-1995.) |
Theorem | ceqsexg 2808* | 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 2809* | Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 29-Dec-1996.) |
Theorem | ceqsrexv 2810* | Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 30-Apr-2004.) |
Theorem | ceqsrexbv 2811* | Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by Mario Carneiro, 14-Mar-2014.) |
Theorem | ceqsrex2v 2812* | Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 29-Oct-2005.) |
Theorem | clel2 2813* | An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.) |
Theorem | clel3g 2814* | An alternate definition of class membership when the class is a set. (Contributed by NM, 13-Aug-2005.) |
Theorem | clel3 2815* | An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.) |
Theorem | clel4 2816* | An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.) |
Theorem | pm13.183 2817* | 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 2818* | Restricted quantifier version of Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 25-Oct-2012.) |
Theorem | rr19.28v 2819* | Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 29-Oct-2012.) |
Theorem | elabgt 2820* | Membership in a class abstraction, using implicit substitution. (Closed theorem version of elabg 2825.) (Contributed by NM, 7-Nov-2005.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Theorem | elabgf 2821 | 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 2822* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 1-Aug-1994.) (Revised by Mario Carneiro, 12-Oct-2016.) |
Theorem | elab 2823* | Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 1-Aug-1994.) |
Theorem | elabd 2824* | Explicit demonstration the class is not empty by the example . (Contributed by RP, 12-Aug-2020.) |
Theorem | elabg 2825* | Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 14-Apr-1995.) |
Theorem | elab2g 2826* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.) |
Theorem | elab2 2827* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.) |
Theorem | elab4g 2828* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 17-Oct-2012.) |
Theorem | elab3gf 2829 | Membership in a class abstraction, with a weaker antecedent than elabgf 2821. (Contributed by NM, 6-Sep-2011.) |
Theorem | elab3g 2830* | Membership in a class abstraction, with a weaker antecedent than elabg 2825. (Contributed by NM, 29-Aug-2006.) |
Theorem | elab3 2831* | Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000.) |
Theorem | elrabi 2832* | Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.) |
Theorem | elrabf 2833 | 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 2834* | Membership in a restricted class abstraction, using implicit substitution. (Closed theorem version of elrab3 2836.) (Contributed by Thierry Arnoux, 31-Aug-2017.) |
Theorem | elrab 2835* | Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.) |
Theorem | elrab3 2836* | Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 5-Oct-2006.) |
Theorem | elrabd 2837* | Membership in a restricted class abstraction, using implicit substitution. Deduction version of elrab 2835. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
Theorem | elrab2 2838* | Membership in a class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.) |
Theorem | ralab 2839* | Universal quantification over a class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | ralrab 2840* | Universal quantification over a restricted class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | rexab 2841* | Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 23-Jan-2014.) (Revised by Mario Carneiro, 3-Sep-2015.) |
Theorem | rexrab 2842* | Existential quantification over a class abstraction. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Mario Carneiro, 3-Sep-2015.) |
Theorem | ralab2 2843* | Universal quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015.) |
Theorem | ralrab2 2844* | Universal quantification over a restricted class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015.) |
Theorem | rexab2 2845* | Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015.) |
Theorem | rexrab2 2846* | Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015.) |
Theorem | abidnf 2847* | 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 2848* | A deduction theorem for converting the inference => into a closed theorem. Use nfa1 1521 and nfab 2284 to eliminate the hypothesis of the substitution instance of the inference. For converting the inference form into a deduction form, abidnf 2847 is useful. (Contributed by NM, 8-Dec-2006.) |
Theorem | eqeu 2849* | A condition which implies existential uniqueness. (Contributed by Jeff Hankins, 8-Sep-2009.) |
Theorem | eueq 2850* | Equality has existential uniqueness. (Contributed by NM, 25-Nov-1994.) |
Theorem | eueq1 2851* | Equality has existential uniqueness. (Contributed by NM, 5-Apr-1995.) |
Theorem | eueq2dc 2852* | Equality has existential uniqueness (split into 2 cases). (Contributed by NM, 5-Apr-1995.) |
DECID | ||
Theorem | eueq3dc 2853* | 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 2854* | There is at most one set equal to a class. (Contributed by NM, 8-Mar-1995.) |
Theorem | moeq3dc 2855* | "At most one" property of equality (split into 3 cases). (Contributed by Jim Kingdon, 7-Jul-2018.) |
DECID DECID | ||
Theorem | mosubt 2856* | "At most one" remains true after substitution. (Contributed by Jim Kingdon, 18-Jan-2019.) |
Theorem | mosub 2857* | "At most one" remains true after substitution. (Contributed by NM, 9-Mar-1995.) |
Theorem | mo2icl 2858* | Theorem for inferring "at most one." (Contributed by NM, 17-Oct-1996.) |
Theorem | mob2 2859* | Consequence of "at most one." (Contributed by NM, 2-Jan-2015.) |
Theorem | moi2 2860* | Consequence of "at most one." (Contributed by NM, 29-Jun-2008.) |
Theorem | mob 2861* | Equality implied by "at most one." (Contributed by NM, 18-Feb-2006.) |
Theorem | moi 2862* | Equality implied by "at most one." (Contributed by NM, 18-Feb-2006.) |
Theorem | morex 2863* | Derive membership from uniqueness. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | euxfr2dc 2864* | Transfer existential uniqueness from a variable to another variable contained in expression . (Contributed by NM, 14-Nov-2004.) |
DECID | ||
Theorem | euxfrdc 2865* | Transfer existential uniqueness from a variable to another variable contained in expression . (Contributed by NM, 14-Nov-2004.) |
DECID | ||
Theorem | euind 2866* | Existential uniqueness via an indirect equality. (Contributed by NM, 11-Oct-2010.) |
Theorem | reu2 2867* | A way to express restricted uniqueness. (Contributed by NM, 22-Nov-1994.) |
Theorem | reu6 2868* | A way to express restricted uniqueness. (Contributed by NM, 20-Oct-2006.) |
Theorem | reu3 2869* | A way to express restricted uniqueness. (Contributed by NM, 24-Oct-2006.) |
Theorem | reu6i 2870* | A condition which implies existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.) |
Theorem | eqreu 2871* | A condition which implies existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.) |
Theorem | rmo4 2872* | Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by NM, 16-Jun-2017.) |
Theorem | reu4 2873* | Restricted uniqueness using implicit substitution. (Contributed by NM, 23-Nov-1994.) |
Theorem | reu7 2874* | Restricted uniqueness using implicit substitution. (Contributed by NM, 24-Oct-2006.) |
Theorem | reu8 2875* | Restricted uniqueness using implicit substitution. (Contributed by NM, 24-Oct-2006.) |
Theorem | rmo3f 2876* | 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 2877* | 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 2878* | Equality has existential uniqueness. (Contributed by Mario Carneiro, 1-Sep-2015.) |
Theorem | rmoan 2879 | Restricted "at most one" still holds when a conjunct is added. (Contributed by NM, 16-Jun-2017.) |
Theorem | rmoim 2880 | Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
Theorem | rmoimia 2881 | Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
Theorem | rmoimi2 2882 | Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
Theorem | 2reuswapdc 2883* | 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 2884* | Existential uniqueness via an indirect equality. (Contributed by NM, 16-Oct-2010.) |
Theorem | 2rmorex 2885* | Double restricted quantification with "at most one," analogous to 2moex 2083. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
Theorem | nelrdva 2886* | 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 2891 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 2896 and cdeqab 2894. | ||
Syntax | wcdeq 2887 | 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 2888 | 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 2889 | Deduce conditional equality. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq | ||
Theorem | cdeqri 2890 | Property of conditional equality. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq | ||
Theorem | cdeqth 2891 | Deduce conditional equality from a theorem. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq | ||
Theorem | cdeqnot 2892 | Distribute conditional equality over negation. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq CondEq | ||
Theorem | cdeqal 2893* | Distribute conditional equality over quantification. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq CondEq | ||
Theorem | cdeqab 2894* | Distribute conditional equality over abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq CondEq | ||
Theorem | cdeqal1 2895* | Distribute conditional equality over quantification. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq CondEq | ||
Theorem | cdeqab1 2896* | Distribute conditional equality over abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq CondEq | ||
Theorem | cdeqim 2897 | Distribute conditional equality over implication. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq CondEq CondEq | ||
Theorem | cdeqcv 2898 | Conditional equality for set-to-class promotion. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq | ||
Theorem | cdeqeq 2899 | Distribute conditional equality over equality. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq CondEq CondEq | ||
Theorem | cdeqel 2900 | Distribute conditional equality over elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.) |
CondEq CondEq CondEq |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |