Home | Metamath
Proof Explorer Theorem List (p. 30 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 | neleq12d 2901 | Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
Theorem | neleq1 2902 | Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
Theorem | neleq2 2903 | Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
Theorem | nfnel 2904 | Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Theorem | nfneld 2905 | Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Theorem | nnel 2906 | Negation of negated membership, analogous to nne 2798. (Contributed by Alexander van der Vekens, 18-Jan-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
Theorem | elnelne1 2907 | Two classes are different if they don't contain the same element. (Contributed by AV, 28-Jan-2020.) |
Theorem | elnelne2 2908 | Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020.) |
Theorem | nelcon3d 2909 | Contrapositive law deduction for negated membership. (Contributed by AV, 28-Jan-2020.) |
Theorem | elnelall 2910 | A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.) |
Theorem | pm2.61danel 2911 | Deduction eliminating an elementhood in an antecedent. (Contributed by AV, 5-Dec-2021.) |
Syntax | wral 2912 | Extend wff notation to include restricted universal quantification. |
Syntax | wrex 2913 | Extend wff notation to include restricted existential quantification. |
Syntax | wreu 2914 | Extend wff notation to include restricted existential uniqueness. |
Syntax | wrmo 2915 | Extend wff notation to include restricted "at most one." |
Syntax | crab 2916 | Extend class notation to include the restricted class abstraction (class builder). |
Definition | df-ral 2917 | Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.) |
Definition | df-rex 2918 | Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.) |
Definition | df-reu 2919 | Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.) |
Definition | df-rmo 2920 | Define restricted "at most one". (Contributed by NM, 16-Jun-2017.) |
Definition | df-rab 2921 | Define a restricted class abstraction (class builder), which is the class of all in such that is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.) |
Theorem | rgen 2922 | Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.) |
Theorem | ralel 2923 | All elements of a class are elements of the class. (Contributed by AV, 30-Oct-2020.) |
Theorem | rgenw 2924 | Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.) |
Theorem | rgen2w 2925 | Generalization rule for restricted quantification. Note that and needn't be distinct. (Contributed by NM, 18-Jun-2014.) |
Theorem | mprg 2926 | Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.) |
Theorem | mprgbir 2927 | Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.) |
Theorem | alral 2928 | Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.) |
Theorem | rsp 2929 | Restricted specialization. (Contributed by NM, 17-Oct-1996.) |
Theorem | rspa 2930 | Restricted specialization. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | rspec 2931 | Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.) |
Theorem | r19.21bi 2932 | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2020.) |
Theorem | r19.21be 2933 | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 21-Nov-1994.) |
Theorem | rspec2 2934 | Specialization rule for restricted quantification, with two quantifiers. (Contributed by NM, 20-Nov-1994.) |
Theorem | rspec3 2935 | Specialization rule for restricted quantification, with three quantifiers. (Contributed by NM, 20-Nov-1994.) |
Theorem | rsp2 2936 | Restricted specialization, with two quantifiers. (Contributed by NM, 11-Feb-1997.) |
Theorem | r2allem 2937 | Lemma factoring out common proof steps of r2alf 2938 and r2al 2939. Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 9-Jan-2020.) |
Theorem | r2alf 2938* | Double restricted universal quantification. (Contributed by Mario Carneiro, 14-Oct-2016.) Use r2allem 2937. (Revised by Wolf Lammen, 9-Jan-2020.) |
Theorem | r2al 2939* | Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Jan-2020.) |
Theorem | r3al 2940* | Triple restricted universal quantification. (Contributed by NM, 19-Nov-1995.) (Proof shortened by Wolf Lammen, 30-Dec-2019.) |
Theorem | nfra1 2941 | The setvar is not free in . (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Theorem | hbra1 2942 | The setvar is not free in . (Contributed by NM, 18-Oct-1996.) (Proof shortened by Wolf Lammen, 7-Dec-2019.) |
Theorem | hbral 2943 | Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by David Abernethy, 13-Dec-2009.) |
Theorem | nfrald 2944 | Deduction version of nfral 2945. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Theorem | nfral 2945 | Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Theorem | nfra2 2946* | Similar to Lemma 24 of [Monk2] p. 114, except the quantification of the antecedent is restricted. Derived automatically from hbra2VD 39096. Contributed by Alan Sare 31-Dec-2011. (Contributed by NM, 31-Dec-2011.) |
Theorem | ral2imi 2947 | Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 2948. (Revised by Wolf Lammen, 1-Dec-2019.) |
Theorem | ralim 2948 | Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.) (Proof shortened by Wolf Lammen, 1-Dec-2019.) |
Theorem | ralimi2 2949 | Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.) |
Theorem | ralimia 2950 | Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.) |
Theorem | ralimiaa 2951 | Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.) |
Theorem | ralimi 2952 | Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.) |
Theorem | 2ralimi 2953 | Inference quantifying both antecedent and consequent two times, with strong hypothesis. (Contributed by AV, 3-Dec-2021.) |
Theorem | hbralrimi 2954 | Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). This theorem contains the common proof steps for ralrimi 2957 and ralrimiv 2965. Its main advantage over these two is its minimal references to axioms. The proof is extracted from NM's previous work. (Contributed by Wolf Lammen, 4-Dec-2019.) |
Theorem | r19.21t 2955 | Restricted quantifier version of 19.21t 2073; closed form of r19.21 2956. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Wolf Lammen, 2-Jan-2020.) |
Theorem | r19.21 2956 | Restricted quantifier version of 19.21 2075. (Contributed by Scott Fenton, 30-Mar-2011.) |
Theorem | ralrimi 2957 | Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 2954. (Revised by Wolf Lammen, 4-Dec-2019.) |
Theorem | ralimdaa 2958 | Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-Sep-2003.) (Proof shortened by Wolf Lammen, 29-Dec-2019.) |
Theorem | ralrimd 2959 | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 16-Feb-2004.) |
Theorem | r19.21v 2960* | Restricted quantifier version of 19.21v 1868. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.) |
Theorem | ralimdv2 2961* | Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.) |
Theorem | ralimdva 2962* | Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.) |
Theorem | ralimdv 2963* | Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1738). (Contributed by NM, 8-Oct-2003.) |
Theorem | ralimdvva 2964* | Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1738). (Contributed by AV, 27-Nov-2019.) |
Theorem | ralrimiv 2965* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 4-Dec-2019.) |
Theorem | ralrimiva 2966* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.) |
Theorem | ralrimivw 2967* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.) |
Theorem | ralrimdv 2968* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 27-May-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Dec-2019.) |
Theorem | ralrimdva 2969* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.) (Proof shortened by Wolf Lammen, 28-Dec-2019.) |
Theorem | ralrimivv 2970* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.) |
Theorem | ralrimivva 2971* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.) |
Theorem | ralrimivvva 2972* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with triple quantification.) (Contributed by Mario Carneiro, 9-Jul-2014.) |
Theorem | ralrimdvv 2973* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 1-Jun-2005.) |
Theorem | ralrimdvva 2974* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 2-Feb-2008.) |
Theorem | rgen2 2975* | Generalization rule for restricted quantification, with two quantifiers. (Contributed by NM, 30-May-1999.) |
Theorem | rgen3 2976* | Generalization rule for restricted quantification, with three quantifiers. (Contributed by NM, 12-Jan-2008.) |
Theorem | rgen2a 2977* | Generalization rule for restricted quantification. Note that and are not required to be disjoint. This proof illustrates the use of dvelim 2337. (Contributed by NM, 23-Nov-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 1-Jan-2020.) (Proof modification is discouraged.) |
Theorem | ralbii2 2978 | Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.) |
Theorem | ralbiia 2979 | Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.) |
Theorem | ralbii 2980 | Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 4-Dec-2019.) |
Theorem | 2ralbii 2981 | Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.) |
Theorem | ralbida 2982 | Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Oct-2003.) |
Theorem | ralbid 2983 | Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.) |
Theorem | ralbidv2 2984* | Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Apr-1997.) |
Theorem | ralbidva 2985* | Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 29-Dec-2019.) |
Theorem | ralbidv 2986* | Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.) |
Theorem | 2ralbida 2987* | Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 24-Feb-2004.) |
Theorem | 2ralbidva 2988* | Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Dec-2019.) |
Theorem | 2ralbidv 2989* | Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.) |
Theorem | raleqbii 2990 | Equality deduction for restricted universal quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.) |
Theorem | raln 2991 | Restricted universally quantified negation expressed as a universally quantified negation. (Contributed by BJ, 16-Jul-2021.) |
Theorem | ralnex 2992 | Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by BJ, 16-Jul-2021.) |
Theorem | ralnexOLD 2993 | Obsolete proof of ralnex 2992 as of 16-Jul-2021. (Contributed by NM, 21-Jan-1997.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | dfral2 2994 | Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) Allow shortening of rexnal 2995. (Revised by Wolf Lammen, 9-Dec-2019.) |
Theorem | rexnal 2995 | Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 9-Dec-2019.) |
Theorem | dfrex2 2996 | Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 26-Nov-2019.) |
Theorem | ralinexa 2997 | A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.) |
Theorem | rexanali 2998 | A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.) (Proof shortened by Wolf Lammen, 27-Dec-2019.) |
Theorem | nrexralim 2999 | Negation of a complex predicate calculus formula. (Contributed by FL, 31-Jul-2009.) |
Theorem | nrex 3000 | Inference adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |