Home | Metamath
Proof Explorer Theorem List (p. 31 of 470) | < 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: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | neeq1d 3001 | Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) | ||
Theorem | neeq2d 3002 | Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) | ||
Theorem | neeq12d 3003 | Deduction for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)) | ||
Theorem | neeq1 3004 | Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) | ||
Theorem | neeq2 3005 | Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) | ||
Theorem | neeq1i 3006 | Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) | ||
Theorem | neeq2i 3007 | Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵) | ||
Theorem | neeq12i 3008 | Inference for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷) | ||
Theorem | eqnetrd 3009 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | eqnetrrd 3010 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐶) | ||
Theorem | neeqtrd 3011 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | eqnetri 3012 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐵 ≠ 𝐶 ⇒ ⊢ 𝐴 ≠ 𝐶 | ||
Theorem | eqnetrri 3013 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐴 ≠ 𝐶 ⇒ ⊢ 𝐵 ≠ 𝐶 | ||
Theorem | neeqtri 3014 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴 ≠ 𝐶 | ||
Theorem | neeqtrri 3015 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴 ≠ 𝐶 | ||
Theorem | neeqtrrd 3016 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | eqnetrrid 3017 | A chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | 3netr3d 3018 | 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 3019 | 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 3020 | Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) | ||
Theorem | 3netr4g 3021 | Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) | ||
Theorem | nebi 3022 | Contraposition law for inequality. (Contributed by NM, 28-Dec-2008.) |
⊢ ((𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ↔ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) | ||
Theorem | pm13.18 3023 | 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 3024 | 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 3025 | Obsolete version of pm13.181 3024 as of 30-Oct-2024. (Contributed by Andrew Salmon, 3-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ≠ 𝐶) → 𝐴 ≠ 𝐶) | ||
Theorem | pm2.61ine 3026 | Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝐴 = 𝐵 → 𝜑) & ⊢ (𝐴 ≠ 𝐵 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | pm2.21ddne 3027 | A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61ne 3028 | 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 3029 | Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61dane 3030 | Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011.) |
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61da2ne 3031 | Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29-May-2013.) |
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓) & ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷)) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61da3ne 3032 | Deduction eliminating three inequalities in an antecedent. (Contributed by NM, 15-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓) & ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝜓) & ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹)) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61iine 3033 | Equality version of pm2.61ii 183. (Contributed by Scott Fenton, 13-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) → 𝜑) & ⊢ (𝐴 = 𝐶 → 𝜑) & ⊢ (𝐵 = 𝐷 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | neor 3034 | Logical OR with an equality. (Contributed by NM, 29-Apr-2007.) |
⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓)) | ||
Theorem | neanior 3035 | A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.) |
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) | ||
Theorem | ne3anior 3036 | A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.) |
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷 ∨ 𝐸 = 𝐹)) | ||
Theorem | neorian 3037 | A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.) |
⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷)) | ||
Theorem | nemtbir 3038 | An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ (𝜑 ↔ 𝐴 = 𝐵) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | nelne1 3039 | 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 3040 | 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 3041 | 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 3042 | 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 3043 | Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵 | ||
Theorem | nfned 3044 | Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 ≠ 𝐵) | ||
Theorem | nabbi 3045 | Not equivalent wff's correspond to not equal class abstractions. (Contributed by AV, 7-Apr-2019.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (∃𝑥(𝜑 ↔ ¬ 𝜓) ↔ {𝑥 ∣ 𝜑} ≠ {𝑥 ∣ 𝜓}) | ||
Theorem | mteqand 3046 | A modus tollens deduction for inequality. (Contributed by Steven Nguyen, 1-Jun-2023.) |
⊢ (𝜑 → 𝐶 ≠ 𝐷) & ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Syntax | wnel 3047 | Extend wff notation to include negated membership. |
wff 𝐴 ∉ 𝐵 | ||
Definition | df-nel 3048 | Define negated membership. (Contributed by NM, 7-Aug-1994.) |
⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | ||
Theorem | neli 3049 | Inference associated with df-nel 3048. (Contributed by BJ, 7-Jul-2018.) |
⊢ 𝐴 ∉ 𝐵 ⇒ ⊢ ¬ 𝐴 ∈ 𝐵 | ||
Theorem | nelir 3050 | Inference associated with df-nel 3048. (Contributed by BJ, 7-Jul-2018.) |
⊢ ¬ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐴 ∉ 𝐵 | ||
Theorem | neleq12d 3051 | Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐷)) | ||
Theorem | neleq1 3052 | Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶)) | ||
Theorem | neleq2 3053 | Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∉ 𝐴 ↔ 𝐶 ∉ 𝐵)) | ||
Theorem | nfnel 3054 | Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ∉ 𝐵 | ||
Theorem | nfneld 3055 | Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∉ 𝐵) | ||
Theorem | nnel 3056 | Negation of negated membership, analogous to nne 2945. (Contributed by Alexander van der Vekens, 18-Jan-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵) | ||
Theorem | elnelne1 3057 | Two classes are different if they don't contain the same element. (Contributed by AV, 28-Jan-2020.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∉ 𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | elnelne2 3058 | Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∉ 𝐶) → 𝐴 ≠ 𝐵) | ||
Theorem | nelcon3d 3059 | Contrapositive law deduction for negated membership. (Contributed by AV, 28-Jan-2020.) |
⊢ (𝜑 → (𝐴 ∈ 𝐵 → 𝐶 ∈ 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 ∉ 𝐷 → 𝐴 ∉ 𝐵)) | ||
Theorem | elnelall 3060 | A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.) |
⊢ (𝐴 ∈ 𝐵 → (𝐴 ∉ 𝐵 → 𝜑)) | ||
Theorem | pm2.61danel 3061 | Deduction eliminating an elementhood in an antecedent. (Contributed by AV, 5-Dec-2021.) |
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐴 ∉ 𝐵) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Syntax | wral 3062 | Extend wff notation to include restricted universal quantification. |
wff ∀𝑥 ∈ 𝐴 𝜑 | ||
Definition | df-ral 3063 |
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 45086 or ralndv2 45087, 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 3064 | Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.) |
⊢ (𝑥 ∈ 𝐴 → 𝜑) ⇒ ⊢ ∀𝑥 ∈ 𝐴 𝜑 | ||
Theorem | ralel 3065 | All elements of a class are elements of the class. (Contributed by AV, 30-Oct-2020.) |
⊢ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐴 | ||
Theorem | rgenw 3066 | Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.) |
⊢ 𝜑 ⇒ ⊢ ∀𝑥 ∈ 𝐴 𝜑 | ||
Theorem | rgen2w 3067 | Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 needn't be distinct. (Contributed by NM, 18-Jun-2014.) |
⊢ 𝜑 ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 | ||
Theorem | mprg 3068 | Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 → 𝜓) & ⊢ (𝑥 ∈ 𝐴 → 𝜑) ⇒ ⊢ 𝜓 | ||
Theorem | mprgbir 3069 | Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.) |
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) & ⊢ (𝑥 ∈ 𝐴 → 𝜓) ⇒ ⊢ 𝜑 | ||
Theorem | raln 3070 | Restricted universally quantified negation expressed as a universally quantified negation. (Contributed by BJ, 16-Jul-2021.) |
⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Syntax | wrex 3071 | Extend wff notation to include restricted existential quantification. |
wff ∃𝑥 ∈ 𝐴 𝜑 | ||
Definition | df-rex 3072 |
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 3063). (Contributed by NM, 30-Aug-1993.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Theorem | ralnex 3073 | Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by BJ, 16-Jul-2021.) |
⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | dfrex2 3074 | Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 26-Nov-2019.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | ||
Theorem | nrex 3075 | Inference adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.) |
⊢ (𝑥 ∈ 𝐴 → ¬ 𝜓) ⇒ ⊢ ¬ ∃𝑥 ∈ 𝐴 𝜓 | ||
Theorem | alral 3076 | Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.) |
⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexex 3077 | Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥𝜑) | ||
Theorem | rextru 3078 | Two ways of expressing that a class has at least one element. (Contributed by Zhi Wang, 23-Sep-2024.) |
⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ⊤) | ||
Theorem | ralimi2 3079 | Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.) |
⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐵 → 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓) | ||
Theorem | reximi2 3080 | Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 8-Nov-2004.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓) | ||
Theorem | ralimia 3081 | Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | reximia 3082 | Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Wolf Lammen, 31-Oct-2024.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralimiaa 3083 | Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralimi 3084 | Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | reximi 3085 | Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ral2imi 3086 | Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 3087. (Revised by Wolf Lammen, 1-Dec-2019.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralim 3087 | Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.) (Proof shortened by Wolf Lammen, 1-Dec-2019.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | rexim 3088 | 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 3089 | Obsolete version of reximia 3082 as of 31-Oct-2024. (Contributed by NM, 10-Feb-1997.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralbii2 3090 | Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.) |
⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐵 → 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓) | ||
Theorem | rexbii2 3091 | Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓) | ||
Theorem | ralbiia 3092 | Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | rexbiia 3093 | Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralbii 3094 | 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 3095 | 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 3096 | Cancellation law for restricted universal quantification. (Contributed by Peter Mazsa, 30-Dec-2018.) (Proof shortened by Wolf Lammen, 29-Jun-2023.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexanid 3097 | Cancellation law for restricted existential quantification. (Contributed by Peter Mazsa, 24-May-2018.) (Proof shortened by Wolf Lammen, 8-Jul-2023.) |
⊢ (∃𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ralcom3 3098 | 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 3099 | Obsolete version of ralcom3 3098 as of 22-Dec-2024. (Contributed by NM, 22-Feb-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 → 𝜑)) | ||
Theorem | dfral2 3100 | Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) Allow shortening of rexnal 3101. (Revised by Wolf Lammen, 9-Dec-2019.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |