![]() |
Metamath
Proof Explorer Theorem List (p. 31 of 485) | < 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-30800) |
![]() (30801-32323) |
![]() (32324-48424) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eqnetrri 3001 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐴 ≠ 𝐶 ⇒ ⊢ 𝐵 ≠ 𝐶 | ||
Theorem | neeqtri 3002 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴 ≠ 𝐶 | ||
Theorem | neeqtrri 3003 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴 ≠ 𝐶 | ||
Theorem | neeqtrrd 3004 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | eqnetrrid 3005 | A chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | 3netr3d 3006 | Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) | ||
Theorem | 3netr4d 3007 | Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 21-Nov-2019.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐴) & ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) | ||
Theorem | 3netr3g 3008 | Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) | ||
Theorem | 3netr4g 3009 | Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) | ||
Theorem | nebi 3010 | Contraposition law for inequality. (Contributed by NM, 28-Dec-2008.) |
⊢ ((𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ↔ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) | ||
Theorem | pm13.18 3011 | Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.) (Proof shortened by Wolf Lammen, 29-Oct-2024.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | pm13.181 3012 | Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Oct-2024.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ≠ 𝐶) → 𝐴 ≠ 𝐶) | ||
Theorem | pm13.181OLD 3013 | Obsolete version of pm13.181 3012 as of 30-Oct-2024. (Contributed by Andrew Salmon, 3-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ≠ 𝐶) → 𝐴 ≠ 𝐶) | ||
Theorem | pm2.61ine 3014 | Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝐴 = 𝐵 → 𝜑) & ⊢ (𝐴 ≠ 𝐵 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | pm2.21ddne 3015 | A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61ne 3016 | Deduction eliminating an inequality in an antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61dne 3017 | Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61dane 3018 | Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011.) |
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61da2ne 3019 | Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29-May-2013.) |
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓) & ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷)) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61da3ne 3020 | Deduction eliminating three inequalities in an antecedent. (Contributed by NM, 15-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓) & ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝜓) & ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹)) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61iine 3021 | Equality version of pm2.61ii 183. (Contributed by Scott Fenton, 13-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) → 𝜑) & ⊢ (𝐴 = 𝐶 → 𝜑) & ⊢ (𝐵 = 𝐷 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | mteqand 3022 | A modus tollens deduction for inequality. (Contributed by Steven Nguyen, 1-Jun-2023.) |
⊢ (𝜑 → 𝐶 ≠ 𝐷) & ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | neor 3023 | Logical OR with an equality. (Contributed by NM, 29-Apr-2007.) |
⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓)) | ||
Theorem | neanior 3024 | A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.) |
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) | ||
Theorem | ne3anior 3025 | A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.) |
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷 ∨ 𝐸 = 𝐹)) | ||
Theorem | neorian 3026 | A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.) |
⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷)) | ||
Theorem | nemtbir 3027 | An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ (𝜑 ↔ 𝐴 = 𝐵) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | nelne1 3028 | Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 14-May-2023.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | nelne2 3029 | Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.) (Proof shortened by Wolf Lammen, 14-May-2023.) |
⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) | ||
Theorem | nelelne 3030 | Two classes are different if they don't belong to the same class. (Contributed by Rodolfo Medina, 17-Oct-2010.) (Proof shortened by AV, 10-May-2020.) |
⊢ (¬ 𝐴 ∈ 𝐵 → (𝐶 ∈ 𝐵 → 𝐶 ≠ 𝐴)) | ||
Theorem | neneor 3031 | If two classes are different, a third class must be different of at least one of them. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
⊢ (𝐴 ≠ 𝐵 → (𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐶)) | ||
Theorem | nfne 3032 | Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵 | ||
Theorem | nfned 3033 | Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 ≠ 𝐵) | ||
Theorem | nabbib 3034 | Not equivalent wff's correspond to not equal class abstractions. (Contributed by AV, 7-Apr-2019.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) Definitial form. (Revised by Wolf Lammen, 5-Mar-2025.) |
⊢ ({𝑥 ∣ 𝜑} ≠ {𝑥 ∣ 𝜓} ↔ ∃𝑥(𝜑 ↔ ¬ 𝜓)) | ||
Syntax | wnel 3035 | Extend wff notation to include negated membership. |
wff 𝐴 ∉ 𝐵 | ||
Definition | df-nel 3036 | Define negated membership. (Contributed by NM, 7-Aug-1994.) |
⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | ||
Theorem | neli 3037 | Inference associated with df-nel 3036. (Contributed by BJ, 7-Jul-2018.) |
⊢ 𝐴 ∉ 𝐵 ⇒ ⊢ ¬ 𝐴 ∈ 𝐵 | ||
Theorem | nelir 3038 | Inference associated with df-nel 3036. (Contributed by BJ, 7-Jul-2018.) |
⊢ ¬ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐴 ∉ 𝐵 | ||
Theorem | nelcon3d 3039 | Contrapositive law deduction for negated membership. (Contributed by AV, 28-Jan-2020.) |
⊢ (𝜑 → (𝐴 ∈ 𝐵 → 𝐶 ∈ 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 ∉ 𝐷 → 𝐴 ∉ 𝐵)) | ||
Theorem | neleq12d 3040 | Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐷)) | ||
Theorem | neleq1 3041 | Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶)) | ||
Theorem | neleq2 3042 | Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∉ 𝐴 ↔ 𝐶 ∉ 𝐵)) | ||
Theorem | nfnel 3043 | Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ∉ 𝐵 | ||
Theorem | nfneld 3044 | Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∉ 𝐵) | ||
Theorem | nnel 3045 | Negation of negated membership, analogous to nne 2933. (Contributed by Alexander van der Vekens, 18-Jan-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵) | ||
Theorem | elnelne1 3046 | Two classes are different if they don't contain the same element. (Contributed by AV, 28-Jan-2020.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∉ 𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | elnelne2 3047 | Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∉ 𝐶) → 𝐴 ≠ 𝐵) | ||
Theorem | pm2.24nel 3048 | A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.) |
⊢ (𝐴 ∈ 𝐵 → (𝐴 ∉ 𝐵 → 𝜑)) | ||
Theorem | pm2.61danel 3049 | Deduction eliminating an elementhood in an antecedent. (Contributed by AV, 5-Dec-2021.) |
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐴 ∉ 𝐵) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Syntax | wral 3050 | Extend wff notation to include restricted universal quantification. |
wff ∀𝑥 ∈ 𝐴 𝜑 | ||
Definition | df-ral 3051 |
Define restricted universal quantification. Special case of Definition
4.15(3) of [TakeutiZaring] p. 22.
Note: This notation is most often used to express that 𝜑 holds for all elements of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint. Should instead 𝐴 depend on 𝑥, you rather focus on those 𝑥 that happen to be contained in the corresponding 𝐴(𝑥). This hardly used interpretation could still occur naturally. For some examples, look at ralndv1 46623 or ralndv2 46624, courtesy of AV. So be careful to either keep 𝐴 independent of 𝑥, or adjust your comments to include such exotic cases. (Contributed by NM, 19-Aug-1993.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | ||
Theorem | rgen 3052 | Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.) |
⊢ (𝑥 ∈ 𝐴 → 𝜑) ⇒ ⊢ ∀𝑥 ∈ 𝐴 𝜑 | ||
Theorem | ralel 3053 | All elements of a class are elements of the class. (Contributed by AV, 30-Oct-2020.) |
⊢ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐴 | ||
Theorem | rgenw 3054 | Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.) |
⊢ 𝜑 ⇒ ⊢ ∀𝑥 ∈ 𝐴 𝜑 | ||
Theorem | rgen2w 3055 | Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 needn't be distinct. (Contributed by NM, 18-Jun-2014.) |
⊢ 𝜑 ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 | ||
Theorem | mprg 3056 | Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 → 𝜓) & ⊢ (𝑥 ∈ 𝐴 → 𝜑) ⇒ ⊢ 𝜓 | ||
Theorem | mprgbir 3057 | Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.) |
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) & ⊢ (𝑥 ∈ 𝐴 → 𝜓) ⇒ ⊢ 𝜑 | ||
Theorem | raln 3058 | Restricted universally quantified negation expressed as a universally quantified negation. (Contributed by BJ, 16-Jul-2021.) |
⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Syntax | wrex 3059 | Extend wff notation to include restricted existential quantification. |
wff ∃𝑥 ∈ 𝐴 𝜑 | ||
Definition | df-rex 3060 |
Define restricted existential quantification. Special case of Definition
4.15(4) of [TakeutiZaring] p. 22.
Note: This notation is most often used to express that 𝜑 holds for at least one element of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint. Should instead 𝐴 depend on 𝑥, you rather assert at least one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3051). (Contributed by NM, 30-Aug-1993.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Theorem | ralnex 3061 | Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by BJ, 16-Jul-2021.) |
⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | dfrex2 3062 | Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 26-Nov-2019.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | ||
Theorem | nrex 3063 | Inference adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.) |
⊢ (𝑥 ∈ 𝐴 → ¬ 𝜓) ⇒ ⊢ ¬ ∃𝑥 ∈ 𝐴 𝜓 | ||
Theorem | alral 3064 | Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.) |
⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexex 3065 | Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥𝜑) | ||
Theorem | rextru 3066 | Two ways of expressing that a class has at least one element. (Contributed by Zhi Wang, 23-Sep-2024.) |
⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ⊤) | ||
Theorem | ralimi2 3067 | Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.) |
⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐵 → 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓) | ||
Theorem | reximi2 3068 | Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 8-Nov-2004.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓) | ||
Theorem | ralimia 3069 | Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | reximia 3070 | Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Wolf Lammen, 31-Oct-2024.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralimiaa 3071 | Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralimi 3072 | Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | reximi 3073 | Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ral2imi 3074 | Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 3075. (Revised by Wolf Lammen, 1-Dec-2019.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralim 3075 | Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.) (Proof shortened by Wolf Lammen, 1-Dec-2019.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | rexim 3076 | Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | reximiaOLD 3077 | Obsolete version of reximia 3070 as of 31-Oct-2024. (Contributed by NM, 10-Feb-1997.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralbii2 3078 | Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.) |
⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐵 → 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓) | ||
Theorem | rexbii2 3079 | Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓) | ||
Theorem | ralbiia 3080 | Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | rexbiia 3081 | Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralbii 3082 | 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 | rexbii 3083 | Inference adding restricted existential 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, 6-Dec-2019.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralanid 3084 | Cancellation law for restricted universal quantification. (Contributed by Peter Mazsa, 30-Dec-2018.) (Proof shortened by Wolf Lammen, 29-Jun-2023.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexanid 3085 | Cancellation law for restricted existential quantification. (Contributed by Peter Mazsa, 24-May-2018.) (Proof shortened by Wolf Lammen, 8-Jul-2023.) |
⊢ (∃𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ralcom3 3086 | A commutation law for restricted universal quantifiers that swaps the domains of the restriction. (Contributed by NM, 22-Feb-2004.) (Proof shortened by Wolf Lammen, 22-Dec-2024.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 → 𝜑)) | ||
Theorem | ralcom3OLD 3087 | Obsolete version of ralcom3 3086 as of 22-Dec-2024. (Contributed by NM, 22-Feb-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 → 𝜑)) | ||
Theorem | dfral2 3088 | Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) Allow shortening of rexnal 3089. (Revised by Wolf Lammen, 9-Dec-2019.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑) | ||
Theorem | rexnal 3089 | Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 9-Dec-2019.) |
⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ralinexa 3090 | A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) | ||
Theorem | rexanali 3091 | A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.) (Proof shortened by Wolf Lammen, 27-Dec-2019.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) | ||
Theorem | ralbi 3092 | Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1812. (Contributed by NM, 6-Oct-2003.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | rexbi 3093 | Distribute restricted quantification over a biconditional. (Contributed by Scott Fenton, 7-Aug-2024.) (Proof shortened by Wolf Lammen, 3-Nov-2024.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | rexbiOLD 3094 | Obsolete version of rexbi 3093 as of 31-Oct-2024. (Contributed by Scott Fenton, 7-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | ralrexbid 3095 | 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 3096 | Obsolete version of ralrexbid 3095 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 3097 | Restricted quantifier version of 19.35 1872. (Contributed by NM, 20-Sep-2003.) (Proof shortened by Wolf Lammen, 22-Dec-2024.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.35OLD 3098 | Obsolete version of 19.35 1872 as of 22-Dec-2024. (Contributed by NM, 20-Sep-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.26m 3099 | Version of 19.26 1865 and r19.26 3100 with restricted quantifiers ranging over different classes. (Contributed by NM, 22-Feb-2004.) |
⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜓)) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | r19.26 3100 | Restricted quantifier version of 19.26 1865. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |