![]() |
Metamath
Proof Explorer Theorem List (p. 32 of 479) | < 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: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rexnal 3101 | Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 9-Dec-2019.) |
β’ (βπ₯ β π΄ Β¬ π β Β¬ βπ₯ β π΄ π) | ||
Theorem | ralinexa 3102 | A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.) |
β’ (βπ₯ β π΄ (π β Β¬ π) β Β¬ βπ₯ β π΄ (π β§ π)) | ||
Theorem | rexanali 3103 | A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.) (Proof shortened by Wolf Lammen, 27-Dec-2019.) |
β’ (βπ₯ β π΄ (π β§ Β¬ π) β Β¬ βπ₯ β π΄ (π β π)) | ||
Theorem | ralbi 3104 | Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1821. (Contributed by NM, 6-Oct-2003.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.) |
β’ (βπ₯ β π΄ (π β π) β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | rexbi 3105 | Distribute restricted quantification over a biconditional. (Contributed by Scott Fenton, 7-Aug-2024.) (Proof shortened by Wolf Lammen, 3-Nov-2024.) |
β’ (βπ₯ β π΄ (π β π) β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | rexbiOLD 3106 | Obsolete version of rexbi 3105 as of 31-Oct-2024. (Contributed by Scott Fenton, 7-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (βπ₯ β π΄ (π β π) β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | ralrexbid 3107 | Formula-building rule for restricted existential quantifier, using a restricted universal quantifier to bind the quantified variable in the antecedent. (Contributed by AV, 21-Oct-2023.) Reduce axiom usage. (Revised by SN, 13-Nov-2023.) (Proof shortened by Wolf Lammen, 4-Nov-2024.) |
β’ (π β (π β π)) β β’ (βπ₯ β π΄ π β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | ralrexbidOLD 3108 | Obsolete version of ralrexbid 3107 as of 4-Nov-2024. (Contributed by AV, 21-Oct-2023.) Reduce axiom usage. (Revised by SN, 13-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β (π β π)) β β’ (βπ₯ β π΄ π β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | r19.35 3109 | Restricted quantifier version of 19.35 1881. (Contributed by NM, 20-Sep-2003.) (Proof shortened by Wolf Lammen, 22-Dec-2024.) |
β’ (βπ₯ β π΄ (π β π) β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | r19.35OLD 3110 | Obsolete version of 19.35 1881 as of 22-Dec-2024. (Contributed by NM, 20-Sep-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (βπ₯ β π΄ (π β π) β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | r19.26m 3111 | Version of 19.26 1874 and r19.26 3112 with restricted quantifiers ranging over different classes. (Contributed by NM, 22-Feb-2004.) |
β’ (βπ₯((π₯ β π΄ β π) β§ (π₯ β π΅ β π)) β (βπ₯ β π΄ π β§ βπ₯ β π΅ π)) | ||
Theorem | r19.26 3112 | Restricted quantifier version of 19.26 1874. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
β’ (βπ₯ β π΄ (π β§ π) β (βπ₯ β π΄ π β§ βπ₯ β π΄ π)) | ||
Theorem | r19.26-3 3113 | Version of r19.26 3112 with three quantifiers. (Contributed by FL, 22-Nov-2010.) |
β’ (βπ₯ β π΄ (π β§ π β§ π) β (βπ₯ β π΄ π β§ βπ₯ β π΄ π β§ βπ₯ β π΄ π)) | ||
Theorem | ralbiim 3114 | Split a biconditional and distribute quantifier. Restricted quantifier version of albiim 1893. (Contributed by NM, 3-Jun-2012.) |
β’ (βπ₯ β π΄ (π β π) β (βπ₯ β π΄ (π β π) β§ βπ₯ β π΄ (π β π))) | ||
Theorem | r19.29 3115 | Restricted quantifier version of 19.29 1877. See also r19.29r 3117. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 22-Dec-2024.) |
β’ ((βπ₯ β π΄ π β§ βπ₯ β π΄ π) β βπ₯ β π΄ (π β§ π)) | ||
Theorem | r19.29OLD 3116 | Obsolete version of r19.29 3115 as of 22-Dec-2024. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((βπ₯ β π΄ π β§ βπ₯ β π΄ π) β βπ₯ β π΄ (π β§ π)) | ||
Theorem | r19.29r 3117 | Restricted quantifier version of 19.29r 1878; variation of r19.29 3115. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Wolf Lammen, 29-Jun-2023.) |
β’ ((βπ₯ β π΄ π β§ βπ₯ β π΄ π) β βπ₯ β π΄ (π β§ π)) | ||
Theorem | r19.29rOLD 3118 | Obsolete version of r19.29r 3117 as of 22-Dec-2024. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Wolf Lammen, 29-Jun-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((βπ₯ β π΄ π β§ βπ₯ β π΄ π) β βπ₯ β π΄ (π β§ π)) | ||
Theorem | r19.29imd 3119 | Theorem 19.29 of [Margaris] p. 90 with an implication in the hypothesis containing the generalization, deduction version. (Contributed by AV, 19-Jan-2019.) |
β’ (π β βπ₯ β π΄ π) & β’ (π β βπ₯ β π΄ (π β π)) β β’ (π β βπ₯ β π΄ (π β§ π)) | ||
Theorem | r19.40 3120 | Restricted quantifier version of Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 2-Apr-2004.) |
β’ (βπ₯ β π΄ (π β§ π) β (βπ₯ β π΄ π β§ βπ₯ β π΄ π)) | ||
Theorem | r19.30 3121 | Restricted quantifier version of 19.30 1885. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof shortened by Wolf Lammen, 5-Nov-2024.) |
β’ (βπ₯ β π΄ (π β¨ π) β (βπ₯ β π΄ π β¨ βπ₯ β π΄ π)) | ||
Theorem | r19.30OLD 3122 | Obsolete version of 19.30 1885 as of 5-Nov-2024. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof shortened by Wolf Lammen, 18-Jun-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (βπ₯ β π΄ (π β¨ π) β (βπ₯ β π΄ π β¨ βπ₯ β π΄ π)) | ||
Theorem | r19.43 3123 | Restricted quantifier version of 19.43 1886. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
β’ (βπ₯ β π΄ (π β¨ π) β (βπ₯ β π΄ π β¨ βπ₯ β π΄ π)) | ||
Theorem | 2ralimi 3124 | Inference quantifying both antecedent and consequent two times, with strong hypothesis. (Contributed by AV, 3-Dec-2021.) |
β’ (π β π) β β’ (βπ₯ β π΄ βπ¦ β π΅ π β βπ₯ β π΄ βπ¦ β π΅ π) | ||
Theorem | 3ralimi 3125 | Inference quantifying both antecedent and consequent three times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025.) |
β’ (π β π) β β’ (βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ π β βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ π) | ||
Theorem | 4ralimi 3126 | Inference quantifying both antecedent and consequent four times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025.) |
β’ (π β π) β β’ (βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ βπ€ β π· π β βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ βπ€ β π· π) | ||
Theorem | 5ralimi 3127 | Inference quantifying both antecedent and consequent five times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025.) |
β’ (π β π) β β’ (βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ βπ€ β π· βπ‘ β πΈ π β βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ βπ€ β π· βπ‘ β πΈ π) | ||
Theorem | 6ralimi 3128 | Inference quantifying both antecedent and consequent six times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025.) |
β’ (π β π) β β’ (βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ βπ€ β π· βπ‘ β πΈ βπ’ β πΉ π β βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ βπ€ β π· βπ‘ β πΈ βπ’ β πΉ π) | ||
Theorem | 2ralbii 3129 | Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.) |
β’ (π β π) β β’ (βπ₯ β π΄ βπ¦ β π΅ π β βπ₯ β π΄ βπ¦ β π΅ π) | ||
Theorem | 2rexbii 3130 | Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.) |
β’ (π β π) β β’ (βπ₯ β π΄ βπ¦ β π΅ π β βπ₯ β π΄ βπ¦ β π΅ π) | ||
Theorem | 3ralbii 3131 | Inference adding three restricted universal quantifiers to both sides of an equivalence. (Contributed by Peter Mazsa, 25-Jul-2019.) |
β’ (π β π) β β’ (βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ π β βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ π) | ||
Theorem | 4ralbii 3132 | Inference adding four restricted universal quantifiers to both sides of an equivalence. (Contributed by Scott Fenton, 28-Feb-2025.) |
β’ (π β π) β β’ (βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ βπ€ β π· π β βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ βπ€ β π· π) | ||
Theorem | 2ralbiim 3133 | Split a biconditional and distribute two restricted universal quantifiers, analogous to 2albiim 1894 and ralbiim 3114. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
β’ (βπ₯ β π΄ βπ¦ β π΅ (π β π) β (βπ₯ β π΄ βπ¦ β π΅ (π β π) β§ βπ₯ β π΄ βπ¦ β π΅ (π β π))) | ||
Theorem | ralnex2 3134 | Relationship between two restricted universal and existential quantifiers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf Lammen, 18-May-2023.) |
β’ (βπ₯ β π΄ βπ¦ β π΅ Β¬ π β Β¬ βπ₯ β π΄ βπ¦ β π΅ π) | ||
Theorem | ralnex3 3135 | Relationship between three restricted universal and existential quantifiers. (Contributed by Thierry Arnoux, 12-Jul-2020.) (Proof shortened by Wolf Lammen, 18-May-2023.) |
β’ (βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ Β¬ π β Β¬ βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ π) | ||
Theorem | rexnal2 3136 | Relationship between two restricted universal and existential quantifiers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (βπ₯ β π΄ βπ¦ β π΅ Β¬ π β Β¬ βπ₯ β π΄ βπ¦ β π΅ π) | ||
Theorem | rexnal3 3137 | Relationship between three restricted universal and existential quantifiers. (Contributed by Thierry Arnoux, 12-Jul-2020.) |
β’ (βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ Β¬ π β Β¬ βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ π) | ||
Theorem | nrexralim 3138 | Negation of a complex predicate calculus formula. (Contributed by FL, 31-Jul-2009.) |
β’ (Β¬ βπ₯ β π΄ βπ¦ β π΅ (π β π) β βπ₯ β π΄ βπ¦ β π΅ (π β§ Β¬ π)) | ||
Theorem | r19.26-2 3139 | Restricted quantifier version of 19.26-2 1875. Version of r19.26 3112 with two quantifiers. (Contributed by NM, 10-Aug-2004.) |
β’ (βπ₯ β π΄ βπ¦ β π΅ (π β§ π) β (βπ₯ β π΄ βπ¦ β π΅ π β§ βπ₯ β π΄ βπ¦ β π΅ π)) | ||
Theorem | 2r19.29 3140 | Theorem r19.29 3115 with two quantifiers. (Contributed by Rodolfo Medina, 25-Sep-2010.) |
β’ ((βπ₯ β π΄ βπ¦ β π΅ π β§ βπ₯ β π΄ βπ¦ β π΅ π) β βπ₯ β π΄ βπ¦ β π΅ (π β§ π)) | ||
Theorem | r19.29d2r 3141 | Theorem 19.29 of [Margaris] p. 90 with two restricted quantifiers, deduction version. (Contributed by Thierry Arnoux, 30-Jan-2017.) (Proof shortened by Wolf Lammen, 4-Nov-2024.) |
β’ (π β βπ₯ β π΄ βπ¦ β π΅ π) & β’ (π β βπ₯ β π΄ βπ¦ β π΅ π) β β’ (π β βπ₯ β π΄ βπ¦ β π΅ (π β§ π)) | ||
Theorem | r19.29d2rOLD 3142 | Obsolete version of r19.29d2r 3141 as of 4-Nov-2024. (Contributed by Thierry Arnoux, 30-Jan-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (π β βπ₯ β π΄ βπ¦ β π΅ π) & β’ (π β βπ₯ β π΄ βπ¦ β π΅ π) β β’ (π β βπ₯ β π΄ βπ¦ β π΅ (π β§ π)) | ||
Theorem | r2allem 3143 | Lemma factoring out common proof steps of r2alf 3279 and r2al 3195. Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 9-Jan-2020.) |
β’ (βπ¦(π₯ β π΄ β (π¦ β π΅ β π)) β (π₯ β π΄ β βπ¦(π¦ β π΅ β π))) β β’ (βπ₯ β π΄ βπ¦ β π΅ π β βπ₯βπ¦((π₯ β π΄ β§ π¦ β π΅) β π)) | ||
Theorem | r2exlem 3144 | Lemma factoring out common proof steps in r2exf 3280 an r2ex 3196. Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 10-Jan-2020.) |
β’ (βπ₯ β π΄ βπ¦ β π΅ Β¬ π β βπ₯βπ¦((π₯ β π΄ β§ π¦ β π΅) β Β¬ π)) β β’ (βπ₯ β π΄ βπ¦ β π΅ π β βπ₯βπ¦((π₯ β π΄ β§ π¦ β π΅) β§ π)) | ||
Theorem | hbralrimi 3145 | Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). This theorem contains the common proof steps for ralrimi 3255 and ralrimiv 3146. 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 | ralrimiv 3146* | 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 3147* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.) |
β’ ((π β§ π₯ β π΄) β π) β β’ (π β βπ₯ β π΄ π) | ||
Theorem | rexlimiva 3148* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.) Shorten dependent theorems. (Revised by Wolf lammen, 23-Dec-2024.) |
β’ ((π₯ β π΄ β§ π) β π) β β’ (βπ₯ β π΄ π β π) | ||
Theorem | rexlimiv 3149* | Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.) |
β’ (π₯ β π΄ β (π β π)) β β’ (βπ₯ β π΄ π β π) | ||
Theorem | nrexdv 3150* | Deduction adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Wolf Lammen, 5-Jan-2020.) |
β’ ((π β§ π₯ β π΄) β Β¬ π) β β’ (π β Β¬ βπ₯ β π΄ π) | ||
Theorem | ralrimivw 3151* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.) |
β’ (π β π) β β’ (π β βπ₯ β π΄ π) | ||
Theorem | rexlimivw 3152* | Weaker version of rexlimiv 3149. (Contributed by FL, 19-Sep-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2024.) |
β’ (π β π) β β’ (βπ₯ β π΄ π β π) | ||
Theorem | ralrimdv 3153* | 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 | rexlimdv 3154* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.) |
β’ (π β (π₯ β π΄ β (π β π))) β β’ (π β (βπ₯ β π΄ π β π)) | ||
Theorem | ralrimdva 3155* | 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 | rexlimdva 3156* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.) |
β’ ((π β§ π₯ β π΄) β (π β π)) β β’ (π β (βπ₯ β π΄ π β π)) | ||
Theorem | rexlimdvaa 3157* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.) |
β’ ((π β§ (π₯ β π΄ β§ π)) β π) β β’ (π β (βπ₯ β π΄ π β π)) | ||
Theorem | rexlimdva2 3158* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (((π β§ π₯ β π΄) β§ π) β π) β β’ (π β (βπ₯ β π΄ π β π)) | ||
Theorem | r19.29an 3159* | A commonly used pattern in the spirit of r19.29 3115. (Contributed by Thierry Arnoux, 29-Dec-2019.) (Proof shortened by Wolf Lammen, 17-Jun-2023.) |
β’ (((π β§ π₯ β π΄) β§ π) β π) β β’ ((π β§ βπ₯ β π΄ π) β π) | ||
Theorem | rexlimdv3a 3160* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 3154. (Contributed by NM, 7-Jun-2015.) |
β’ ((π β§ π₯ β π΄ β§ π) β π) β β’ (π β (βπ₯ β π΄ π β π)) | ||
Theorem | rexlimdvw 3161* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Jun-2014.) |
β’ (π β (π β π)) β β’ (π β (βπ₯ β π΄ π β π)) | ||
Theorem | rexlimddv 3162* | Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.) |
β’ (π β βπ₯ β π΄ π) & β’ ((π β§ (π₯ β π΄ β§ π)) β π) β β’ (π β π) | ||
Theorem | r19.29a 3163* | A commonly used pattern in the spirit of r19.29 3115. (Contributed by Thierry Arnoux, 22-Nov-2017.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.) |
β’ (((π β§ π₯ β π΄) β§ π) β π) & β’ (π β βπ₯ β π΄ π) β β’ (π β π) | ||
Theorem | ralimdv2 3164* | Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.) |
β’ (π β ((π₯ β π΄ β π) β (π₯ β π΅ β π))) β β’ (π β (βπ₯ β π΄ π β βπ₯ β π΅ π)) | ||
Theorem | reximdv2 3165* | Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.) |
β’ (π β ((π₯ β π΄ β§ π) β (π₯ β π΅ β§ π))) β β’ (π β (βπ₯ β π΄ π β βπ₯ β π΅ π)) | ||
Theorem | reximdvai 3166* | Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 14-Nov-2002.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 8-Jan-2020.) (Proof shortened by Wolf Lammen, 4-Nov-2024.) |
β’ (π β (π₯ β π΄ β (π β π))) β β’ (π β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | reximdvaiOLD 3167* | Obsolete version of reximdvai 3166 as of 3-Nov-2024. (Contributed by NM, 14-Nov-2002.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 8-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β (π₯ β π΄ β (π β π))) β β’ (π β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | ralimdva 3168* | 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 | reximdva 3169* | Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.) |
β’ ((π β§ π₯ β π΄) β (π β π)) β β’ (π β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | ralimdv 3170* | Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1813). (Contributed by NM, 8-Oct-2003.) |
β’ (π β (π β π)) β β’ (π β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | reximdv 3171* | Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.) |
β’ (π β (π β π)) β β’ (π β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | reximddv 3172* | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
β’ ((π β§ (π₯ β π΄ β§ π)) β π) & β’ (π β βπ₯ β π΄ π) β β’ (π β βπ₯ β π΄ π) | ||
Theorem | reximssdv 3173* | Derivation of a restricted existential quantification over a subset (the second hypothesis implies π΄ β π΅), deduction form. (Contributed by AV, 21-Aug-2022.) |
β’ (π β βπ₯ β π΅ π) & β’ ((π β§ (π₯ β π΅ β§ π)) β π₯ β π΄) & β’ ((π β§ (π₯ β π΅ β§ π)) β π) β β’ (π β βπ₯ β π΄ π) | ||
Theorem | ralbidv2 3174* | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Apr-1997.) |
β’ (π β ((π₯ β π΄ β π) β (π₯ β π΅ β π))) β β’ (π β (βπ₯ β π΄ π β βπ₯ β π΅ π)) | ||
Theorem | rexbidv2 3175* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 22-May-1999.) |
β’ (π β ((π₯ β π΄ β§ π) β (π₯ β π΅ β§ π))) β β’ (π β (βπ₯ β π΄ π β βπ₯ β π΅ π)) | ||
Theorem | ralbidva 3176* | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 29-Dec-2019.) |
β’ ((π β§ π₯ β π΄) β (π β π)) β β’ (π β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | rexbidva 3177* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Dec-2019.) |
β’ ((π β§ π₯ β π΄) β (π β π)) β β’ (π β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | ralbidv 3178* | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.) |
β’ (π β (π β π)) β β’ (π β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | rexbidv 3179* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.) |
β’ (π β (π β π)) β β’ (π β (βπ₯ β π΄ π β βπ₯ β π΄ π)) | ||
Theorem | r19.21v 3180* | Restricted quantifier version of 19.21v 1943. (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.) (Proof shortened by Wolf Lammen, 11-Dec-2024.) |
β’ (βπ₯ β π΄ (π β π) β (π β βπ₯ β π΄ π)) | ||
Theorem | r19.21vOLD 3181* | Obsolete version of r19.21v 3180 as of 11-Dec-2024. (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.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (βπ₯ β π΄ (π β π) β (π β βπ₯ β π΄ π)) | ||
Theorem | r19.37v 3182* | Restricted quantifier version of one direction of 19.37v 1996. (The other direction holds iff π΄ is nonempty, see r19.37zv 4502.) (Contributed by NM, 2-Apr-2004.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Jun-2023.) |
β’ (βπ₯ β π΄ (π β π) β (π β βπ₯ β π΄ π)) | ||
Theorem | r19.23v 3183* | Restricted quantifier version of 19.23v 1946. Version of r19.23 3254 with a disjoint variable condition. (Contributed by NM, 31-Aug-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.) |
β’ (βπ₯ β π΄ (π β π) β (βπ₯ β π΄ π β π)) | ||
Theorem | r19.36v 3184* | Restricted quantifier version of one direction of 19.36 2224. (The other direction holds iff π΄ is nonempty, see r19.36zv 4507.) (Contributed by NM, 22-Oct-2003.) |
β’ (βπ₯ β π΄ (π β π) β (βπ₯ β π΄ π β π)) | ||
Theorem | rexlimivOLD 3185* | Obsolete version of rexlimiv 3149 as of 19-Dec-2024.) (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π₯ β π΄ β (π β π)) β β’ (βπ₯ β π΄ π β π) | ||
Theorem | rexlimivaOLD 3186* | Obsolete version of rexlimiva 3148 as of 23-Dec-2024. (Contributed by NM, 18-Dec-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π₯ β π΄ β§ π) β π) β β’ (βπ₯ β π΄ π β π) | ||
Theorem | rexlimivwOLD 3187* | Obsolete version of rexlimivw 3152 as of 23-Dec-2024. (Contributed by FL, 19-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π) β β’ (βπ₯ β π΄ π β π) | ||
Theorem | r19.27v 3188* | Restricted quantitifer version of one direction of 19.27 2221. (Assuming β²π₯π΄, the other direction holds when π΄ is nonempty, see r19.27zv 4506.) (Contributed by NM, 3-Jun-2004.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 17-Jun-2023.) |
β’ ((βπ₯ β π΄ π β§ π) β βπ₯ β π΄ (π β§ π)) | ||
Theorem | r19.41v 3189* | Restricted quantifier version 19.41v 1954. Version of r19.41 3261 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 17-Dec-2003.) Reduce dependencies on axioms. (Revised by BJ, 29-Mar-2020.) |
β’ (βπ₯ β π΄ (π β§ π) β (βπ₯ β π΄ π β§ π)) | ||
Theorem | r19.28v 3190* | Restricted quantifier version of one direction of 19.28 2222. (Assuming β²π₯π΄, the other direction holds when π΄ is nonempty, see r19.28zv 4501.) (Contributed by NM, 2-Apr-2004.) (Proof shortened by Wolf Lammen, 17-Jun-2023.) |
β’ ((π β§ βπ₯ β π΄ π) β βπ₯ β π΄ (π β§ π)) | ||
Theorem | r19.42v 3191* | Restricted quantifier version of 19.42v 1958 (see also 19.42 2230). (Contributed by NM, 27-May-1998.) |
β’ (βπ₯ β π΄ (π β§ π) β (π β§ βπ₯ β π΄ π)) | ||
Theorem | r19.32v 3192* | Restricted quantifier version of 19.32v 1944. (Contributed by NM, 25-Nov-2003.) |
β’ (βπ₯ β π΄ (π β¨ π) β (π β¨ βπ₯ β π΄ π)) | ||
Theorem | r19.45v 3193* | Restricted quantifier version of one direction of 19.45 2232. The other direction holds when π΄ is nonempty, see r19.45zv 4503. (Contributed by NM, 2-Apr-2004.) |
β’ (βπ₯ β π΄ (π β¨ π) β (π β¨ βπ₯ β π΄ π)) | ||
Theorem | r19.44v 3194* | One direction of a restricted quantifier version of 19.44 2231. The other direction holds when π΄ is nonempty, see r19.44zv 4504. (Contributed by NM, 2-Apr-2004.) |
β’ (βπ₯ β π΄ (π β¨ π) β (βπ₯ β π΄ π β¨ π)) | ||
Theorem | r2al 3195* | Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Jan-2020.) |
β’ (βπ₯ β π΄ βπ¦ β π΅ π β βπ₯βπ¦((π₯ β π΄ β§ π¦ β π΅) β π)) | ||
Theorem | r2ex 3196* | Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 10-Jan-2020.) |
β’ (βπ₯ β π΄ βπ¦ β π΅ π β βπ₯βπ¦((π₯ β π΄ β§ π¦ β π΅) β§ π)) | ||
Theorem | r3al 3197* | Triple restricted universal quantification. (Contributed by NM, 19-Nov-1995.) (Proof shortened by Wolf Lammen, 30-Dec-2019.) |
β’ (βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ π β βπ₯βπ¦βπ§((π₯ β π΄ β§ π¦ β π΅ β§ π§ β πΆ) β π)) | ||
Theorem | rgen2 3198* | Generalization rule for restricted quantification, with two quantifiers. This theorem should be used in place of rgen2a 3368 since it depends on a smaller set of axioms. (Contributed by NM, 30-May-1999.) |
β’ ((π₯ β π΄ β§ π¦ β π΅) β π) β β’ βπ₯ β π΄ βπ¦ β π΅ π | ||
Theorem | ralrimivv 3199* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.) |
β’ (π β ((π₯ β π΄ β§ π¦ β π΅) β π)) β β’ (π β βπ₯ β π΄ βπ¦ β π΅ π) | ||
Theorem | rexlimivv 3200* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.) |
β’ ((π₯ β π΄ β§ π¦ β π΅) β (π β π)) β β’ (βπ₯ β π΄ βπ¦ β π΅ π β π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |