![]() |
Metamath
Proof Explorer Theorem List (p. 31 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | necon3i 3001 | Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.) (Proof shortened by Wolf Lammen, 22-Nov-2019.) |
⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵) | ||
Theorem | necon1i 3002 | Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.) |
⊢ (𝐴 ≠ 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ (𝐶 ≠ 𝐷 → 𝐴 = 𝐵) | ||
Theorem | necon2i 3003 | Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.) |
⊢ (𝐴 = 𝐵 → 𝐶 ≠ 𝐷) ⇒ ⊢ (𝐶 = 𝐷 → 𝐴 ≠ 𝐵) | ||
Theorem | necon4i 3004 | Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2019.) |
⊢ (𝐴 ≠ 𝐵 → 𝐶 ≠ 𝐷) ⇒ ⊢ (𝐶 = 𝐷 → 𝐴 = 𝐵) | ||
Theorem | necon3abid 3005 | Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.) |
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) | ||
Theorem | necon3bbid 3006 | Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.) |
⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)) | ||
Theorem | necon1abid 3007 | Contrapositive deduction for inequality. (Contributed by NM, 21-Aug-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.) |
⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝜓)) | ||
Theorem | necon1bbid 3008 | Contrapositive inference for inequality. (Contributed by NM, 31-Jan-2008.) |
⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝜓)) ⇒ ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 = 𝐵)) | ||
Theorem | necon4abid 3009 | Contrapositive law deduction for inequality. (Contributed by NM, 11-Jan-2008.) (Proof shortened by Wolf Lammen, 24-Nov-2019.) |
⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) | ||
Theorem | necon4bbid 3010 | Contrapositive law deduction for inequality. (Contributed by NM, 9-May-2012.) |
⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵)) | ||
Theorem | necon2abid 3011 | Contrapositive deduction for inequality. (Contributed by NM, 18-Jul-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.) |
⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵)) | ||
Theorem | necon2bbid 3012 | Contrapositive deduction for inequality. (Contributed by NM, 13-Apr-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓)) | ||
Theorem | necon3bid 3013 | Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) | ||
Theorem | necon4bid 3014 | Contrapositive law deduction for inequality. (Contributed by NM, 29-Jun-2007.) |
⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)) | ||
Theorem | necon3abii 3015 | Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.) |
⊢ (𝐴 = 𝐵 ↔ 𝜑) ⇒ ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑) | ||
Theorem | necon3bbii 3016 | Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.) |
⊢ (𝜑 ↔ 𝐴 = 𝐵) ⇒ ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵) | ||
Theorem | necon1abii 3017 | Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (¬ 𝜑 ↔ 𝐴 = 𝐵) ⇒ ⊢ (𝐴 ≠ 𝐵 ↔ 𝜑) | ||
Theorem | necon1bbii 3018 | Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.) |
⊢ (𝐴 ≠ 𝐵 ↔ 𝜑) ⇒ ⊢ (¬ 𝜑 ↔ 𝐴 = 𝐵) | ||
Theorem | necon2abii 3019 | Contrapositive inference for inequality. (Contributed by NM, 2-Mar-2007.) |
⊢ (𝐴 = 𝐵 ↔ ¬ 𝜑) ⇒ ⊢ (𝜑 ↔ 𝐴 ≠ 𝐵) | ||
Theorem | necon2bbii 3020 | Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.) |
⊢ (𝜑 ↔ 𝐴 ≠ 𝐵) ⇒ ⊢ (𝐴 = 𝐵 ↔ ¬ 𝜑) | ||
Theorem | necon3bii 3021 | Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.) |
⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ⇒ ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) | ||
Theorem | necom 3022 | Commutation of inequality. (Contributed by NM, 14-May-1999.) |
⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) | ||
Theorem | necomi 3023 | Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.) |
⊢ 𝐴 ≠ 𝐵 ⇒ ⊢ 𝐵 ≠ 𝐴 | ||
Theorem | necomd 3024 | Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐴) | ||
Theorem | nesym 3025 | Characterization of inequality in terms of reversed equality (see bicom 214). (Contributed by BJ, 7-Jul-2018.) |
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) | ||
Theorem | nesymi 3026 | Inference associated with nesym 3025. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ 𝐴 ≠ 𝐵 ⇒ ⊢ ¬ 𝐵 = 𝐴 | ||
Theorem | nesymir 3027 | Inference associated with nesym 3025. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ ¬ 𝐴 = 𝐵 ⇒ ⊢ 𝐵 ≠ 𝐴 | ||
Theorem | neeq1d 3028 | Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) | ||
Theorem | neeq2d 3029 | Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) | ||
Theorem | neeq12d 3030 | Deduction for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)) | ||
Theorem | neeq1 3031 | Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) | ||
Theorem | neeq2 3032 | Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) | ||
Theorem | neeq1i 3033 | Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) | ||
Theorem | neeq2i 3034 | Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵) | ||
Theorem | neeq12i 3035 | Inference for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷) | ||
Theorem | eqnetrd 3036 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | eqnetrrd 3037 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐶) | ||
Theorem | neeqtrd 3038 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | eqnetri 3039 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐵 ≠ 𝐶 ⇒ ⊢ 𝐴 ≠ 𝐶 | ||
Theorem | eqnetrri 3040 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐴 ≠ 𝐶 ⇒ ⊢ 𝐵 ≠ 𝐶 | ||
Theorem | neeqtri 3041 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴 ≠ 𝐶 | ||
Theorem | neeqtrri 3042 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴 ≠ 𝐶 | ||
Theorem | neeqtrrd 3043 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | syl5eqner 3044 | A chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | 3netr3d 3045 | 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 3046 | 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 3047 | Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) | ||
Theorem | 3netr4g 3048 | Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) | ||
Theorem | nebi 3049 | Contraposition law for inequality. (Contributed by NM, 28-Dec-2008.) |
⊢ ((𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ↔ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) | ||
Theorem | pm13.18 3050 | Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.) (Proof shortened by Wolf Lammen, 14-May-2023.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | pm13.18OLD 3051 | Obsolete version of pm13.18 3050 as of 14-May-2023. (Contributed by Andrew Salmon, 3-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | pm13.181 3052 | Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ≠ 𝐶) → 𝐴 ≠ 𝐶) | ||
Theorem | pm2.61ine 3053 | Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝐴 = 𝐵 → 𝜑) & ⊢ (𝐴 ≠ 𝐵 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | pm2.21ddne 3054 | A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61ne 3055 | 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 3056 | Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61dane 3057 | Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011.) |
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61da2ne 3058 | Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29-May-2013.) |
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓) & ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷)) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61da3ne 3059 | Deduction eliminating three inequalities in an antecedent. (Contributed by NM, 15-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓) & ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝜓) & ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹)) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61iine 3060 | Equality version of pm2.61ii 178. (Contributed by Scott Fenton, 13-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) → 𝜑) & ⊢ (𝐴 = 𝐶 → 𝜑) & ⊢ (𝐵 = 𝐷 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | neor 3061 | Logical OR with an equality. (Contributed by NM, 29-Apr-2007.) |
⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓)) | ||
Theorem | neanior 3062 | A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.) |
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) | ||
Theorem | ne3anior 3063 | A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.) |
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷 ∨ 𝐸 = 𝐹)) | ||
Theorem | neorian 3064 | A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.) |
⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷)) | ||
Theorem | nemtbir 3065 | An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ (𝜑 ↔ 𝐴 = 𝐵) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | nelne1 3066 | 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 | nelne1OLD 3067 | Obsolete version of nelne1 3066 asw of 14-May-2023. (Contributed by NM, 3-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | nelne2 3068 | 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 | nelne2OLD 3069 | Obsolete version of nelne2 3068 asw of 14-May-2023. (Contributed by NM, 25-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) | ||
Theorem | nelelne 3070 | 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 3071 | 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 3072 | Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵 | ||
Theorem | nfned 3073 | Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 ≠ 𝐵) | ||
Theorem | nabbi 3074 | Not equivalent wff's correspond to not equal class abstractions. (Contributed by AV, 7-Apr-2019.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (∃𝑥(𝜑 ↔ ¬ 𝜓) ↔ {𝑥 ∣ 𝜑} ≠ {𝑥 ∣ 𝜓}) | ||
Syntax | wnel 3075 | Extend wff notation to include negated membership. |
wff 𝐴 ∉ 𝐵 | ||
Definition | df-nel 3076 | Define negated membership. (Contributed by NM, 7-Aug-1994.) |
⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | ||
Theorem | neli 3077 | Inference associated with df-nel 3076. (Contributed by BJ, 7-Jul-2018.) |
⊢ 𝐴 ∉ 𝐵 ⇒ ⊢ ¬ 𝐴 ∈ 𝐵 | ||
Theorem | nelir 3078 | Inference associated with df-nel 3076. (Contributed by BJ, 7-Jul-2018.) |
⊢ ¬ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐴 ∉ 𝐵 | ||
Theorem | neleq12d 3079 | Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐷)) | ||
Theorem | neleq1 3080 | Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶)) | ||
Theorem | neleq2 3081 | Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∉ 𝐴 ↔ 𝐶 ∉ 𝐵)) | ||
Theorem | nfnel 3082 | Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ∉ 𝐵 | ||
Theorem | nfneld 3083 | Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∉ 𝐵) | ||
Theorem | nnel 3084 | Negation of negated membership, analogous to nne 2973. (Contributed by Alexander van der Vekens, 18-Jan-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵) | ||
Theorem | elnelne1 3085 | Two classes are different if they don't contain the same element. (Contributed by AV, 28-Jan-2020.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∉ 𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | elnelne2 3086 | Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∉ 𝐶) → 𝐴 ≠ 𝐵) | ||
Theorem | nelcon3d 3087 | Contrapositive law deduction for negated membership. (Contributed by AV, 28-Jan-2020.) |
⊢ (𝜑 → (𝐴 ∈ 𝐵 → 𝐶 ∈ 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 ∉ 𝐷 → 𝐴 ∉ 𝐵)) | ||
Theorem | elnelall 3088 | A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.) |
⊢ (𝐴 ∈ 𝐵 → (𝐴 ∉ 𝐵 → 𝜑)) | ||
Theorem | pm2.61danel 3089 | Deduction eliminating an elementhood in an antecedent. (Contributed by AV, 5-Dec-2021.) |
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐴 ∉ 𝐵) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Syntax | wral 3090 | Extend wff notation to include restricted universal quantification. |
wff ∀𝑥 ∈ 𝐴 𝜑 | ||
Syntax | wrex 3091 | Extend wff notation to include restricted existential quantification. |
wff ∃𝑥 ∈ 𝐴 𝜑 | ||
Syntax | wreu 3092 | Extend wff notation to include restricted existential uniqueness. |
wff ∃!𝑥 ∈ 𝐴 𝜑 | ||
Syntax | wrmo 3093 | Extend wff notation to include restricted "at most one." |
wff ∃*𝑥 ∈ 𝐴 𝜑 | ||
Syntax | crab 3094 | Extend class notation to include the restricted class abstraction (class builder). |
class {𝑥 ∈ 𝐴 ∣ 𝜑} | ||
Definition | df-ral 3095 | Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | ||
Definition | df-rex 3096 | Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Definition | df-reu 3097 | Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Definition | df-rmo 3098 | Define restricted "at most one". (Contributed by NM, 16-Jun-2017.) |
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Definition | df-rab 3099 | 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 | ralanid 3100 | Cancellation law for restricted universal quantification. (Contributed by Peter Mazsa, 30-Dec-2018.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |