Home | Metamath
Proof Explorer Theorem List (p. 31 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nfabd 3001 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.) Avoid ax-9 2115 and ax-ext 2793. (Revised by Wolf Lammen, 23-May-2023.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓}) | ||
Theorem | nfabd2 3002 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.) (Proof shortened by Wolf Lammen, 10-May-2023.) |
⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓}) | ||
Theorem | nfabd2OLD 3003 | Obsolete version of nfabd2 3002 as of 23-May-2023. (Contributed by Mario Carneiro, 8-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓}) | ||
Theorem | nfabdOLD 3004 | Obsolete version of nfabd 3001 as of 10-May-2023. (Contributed by Mario Carneiro, 8-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓}) | ||
Theorem | dvelimdc 3005 | Deduction form of dvelimc 3006. (Contributed by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑧𝐵) & ⊢ (𝜑 → (𝑧 = 𝑦 → 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵)) | ||
Theorem | dvelimc 3006 | Version of dvelim 2468 for classes. (Contributed by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑧𝐵 & ⊢ (𝑧 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵) | ||
Theorem | nfcvf 3007 | If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. (Contributed by Mario Carneiro, 8-Oct-2016.) Avoid ax-ext 2793. (Revised by Wolf Lammen, 10-May-2023.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) | ||
Theorem | nfcvf2 3008 | If 𝑥 and 𝑦 are distinct, then 𝑦 is not free in 𝑥. (Contributed by Mario Carneiro, 5-Dec-2016.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) | ||
Theorem | nfcvfOLD 3009 | Obsolete version of nfcvf 3007 as of 10-May-2023. (Contributed by Mario Carneiro, 8-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) | ||
Theorem | cleqf 3010 | Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions as in dfcleq 2815. See also cleqh 2936. (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Nov-2019.) Avoid ax-13 2383. (Revised by Wolf Lammen, 10-May-2023.) Avoid ax-10 2136. (Revised by Gino Giotto, 20-Aug-2023.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | cleqfOLD 3011 | Obsolete version of cleqf 3010 as of 10-May-2023. (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Nov-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | abid2f 3012 | A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 5-Sep-2011.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Nov-2019.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 | ||
Theorem | abeq2f 3013 | Equality of a class variable and a class abstraction. In this version, the fact that 𝑥 is a non-free variable in 𝐴 is explicitly stated as a hypothesis. (Contributed by Thierry Arnoux, 11-May-2017.) Avoid ax-13 2383. (Revised by Wolf Lammen, 13-May-2023.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑)) | ||
Theorem | abeq2fOLD 3014 | Obsolete version of abeq2f 3013 as of 13-May-2023. (Contributed by Thierry Arnoux, 11-May-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑)) | ||
Theorem | sbabel 3015* | Theorem to move a substitution in and out of a class abstraction. (Contributed by NM, 27-Sep-2003.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 26-Dec-2019.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ ([𝑦 / 𝑥]{𝑧 ∣ 𝜑} ∈ 𝐴 ↔ {𝑧 ∣ [𝑦 / 𝑥]𝜑} ∈ 𝐴) | ||
Syntax | wne 3016 | Extend wff notation to include inequality. |
wff 𝐴 ≠ 𝐵 | ||
Definition | df-ne 3017 | Define inequality. (Contributed by NM, 26-May-1993.) |
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | ||
Theorem | neii 3018 | Inference associated with df-ne 3017. (Contributed by BJ, 7-Jul-2018.) |
⊢ 𝐴 ≠ 𝐵 ⇒ ⊢ ¬ 𝐴 = 𝐵 | ||
Theorem | neir 3019 | Inference associated with df-ne 3017. (Contributed by BJ, 7-Jul-2018.) |
⊢ ¬ 𝐴 = 𝐵 ⇒ ⊢ 𝐴 ≠ 𝐵 | ||
Theorem | nne 3020 | Negation of inequality. (Contributed by NM, 9-Jun-2006.) |
⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | ||
Theorem | neneqd 3021 | Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐴 = 𝐵) | ||
Theorem | neneq 3022 | From inequality to non-equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵) | ||
Theorem | neqned 3023 | If it is not the case that two classes are equal, then they are unequal. Converse of neneqd 3021. One-way deduction form of df-ne 3017. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 3042. (Revised by Wolf Lammen, 22-Nov-2019.) |
⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | neqne 3024 | From non-equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵) | ||
Theorem | neirr 3025 | No class is unequal to itself. Inequality is irreflexive. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ ¬ 𝐴 ≠ 𝐴 | ||
Theorem | exmidne 3026 | Excluded middle with equality and inequality. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 17-Nov-2019.) |
⊢ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵) | ||
Theorem | eqneqall 3027 | A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.) |
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑)) | ||
Theorem | nonconne 3028 | Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 21-Dec-2019.) |
⊢ ¬ (𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐵) | ||
Theorem | necon3ad 3029 | Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓)) | ||
Theorem | necon3bd 3030 | Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) ⇒ ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵)) | ||
Theorem | necon2ad 3031 | Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) ⇒ ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) | ||
Theorem | necon2bd 3032 | Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.) |
⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) | ||
Theorem | necon1ad 3033 | Contrapositive deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) | ||
Theorem | necon1bd 3034 | Contrapositive deduction for inequality. (Contributed by NM, 21-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) ⇒ ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵)) | ||
Theorem | necon4ad 3035 | Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓)) ⇒ ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) | ||
Theorem | necon4bd 3036 | Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) | ||
Theorem | necon3d 3037 | Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.) |
⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 = 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵)) | ||
Theorem | necon1d 3038 | Contrapositive law deduction for inequality. (Contributed by NM, 28-Dec-2008.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝐶 = 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵)) | ||
Theorem | necon2d 3039 | Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.) |
⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 ≠ 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 ≠ 𝐵)) | ||
Theorem | necon4d 3040 | Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝐶 ≠ 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 = 𝐵)) | ||
Theorem | necon3ai 3041 | Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑) | ||
Theorem | necon3bi 3042 | Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.) |
⊢ (𝐴 = 𝐵 → 𝜑) ⇒ ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | necon1ai 3043 | Contrapositive inference for inequality. (Contributed by NM, 12-Feb-2007.) (Proof shortened by Wolf Lammen, 22-Nov-2019.) |
⊢ (¬ 𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝐴 ≠ 𝐵 → 𝜑) | ||
Theorem | necon1bi 3044 | Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.) |
⊢ (𝐴 ≠ 𝐵 → 𝜑) ⇒ ⊢ (¬ 𝜑 → 𝐴 = 𝐵) | ||
Theorem | necon2ai 3045 | Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.) |
⊢ (𝐴 = 𝐵 → ¬ 𝜑) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | necon2bi 3046 | Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝐴 = 𝐵 → ¬ 𝜑) | ||
Theorem | necon4ai 3047 | Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.) |
⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | necon3i 3048 | Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.) (Proof shortened by Wolf Lammen, 22-Nov-2019.) |
⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵) | ||
Theorem | necon1i 3049 | Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.) |
⊢ (𝐴 ≠ 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ (𝐶 ≠ 𝐷 → 𝐴 = 𝐵) | ||
Theorem | necon2i 3050 | Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.) |
⊢ (𝐴 = 𝐵 → 𝐶 ≠ 𝐷) ⇒ ⊢ (𝐶 = 𝐷 → 𝐴 ≠ 𝐵) | ||
Theorem | necon4i 3051 | 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 3052 | Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.) |
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) | ||
Theorem | necon3bbid 3053 | Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.) |
⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)) | ||
Theorem | necon1abid 3054 | Contrapositive deduction for inequality. (Contributed by NM, 21-Aug-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.) |
⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝜓)) | ||
Theorem | necon1bbid 3055 | Contrapositive inference for inequality. (Contributed by NM, 31-Jan-2008.) |
⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝜓)) ⇒ ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 = 𝐵)) | ||
Theorem | necon4abid 3056 | Contrapositive law deduction for inequality. (Contributed by NM, 11-Jan-2008.) (Proof shortened by Wolf Lammen, 24-Nov-2019.) |
⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) | ||
Theorem | necon4bbid 3057 | Contrapositive law deduction for inequality. (Contributed by NM, 9-May-2012.) |
⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵)) | ||
Theorem | necon2abid 3058 | Contrapositive deduction for inequality. (Contributed by NM, 18-Jul-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.) |
⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵)) | ||
Theorem | necon2bbid 3059 | Contrapositive deduction for inequality. (Contributed by NM, 13-Apr-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓)) | ||
Theorem | necon3bid 3060 | Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) | ||
Theorem | necon4bid 3061 | Contrapositive law deduction for inequality. (Contributed by NM, 29-Jun-2007.) |
⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)) | ||
Theorem | necon3abii 3062 | Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.) |
⊢ (𝐴 = 𝐵 ↔ 𝜑) ⇒ ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑) | ||
Theorem | necon3bbii 3063 | Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.) |
⊢ (𝜑 ↔ 𝐴 = 𝐵) ⇒ ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵) | ||
Theorem | necon1abii 3064 | Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (¬ 𝜑 ↔ 𝐴 = 𝐵) ⇒ ⊢ (𝐴 ≠ 𝐵 ↔ 𝜑) | ||
Theorem | necon1bbii 3065 | Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.) |
⊢ (𝐴 ≠ 𝐵 ↔ 𝜑) ⇒ ⊢ (¬ 𝜑 ↔ 𝐴 = 𝐵) | ||
Theorem | necon2abii 3066 | Contrapositive inference for inequality. (Contributed by NM, 2-Mar-2007.) |
⊢ (𝐴 = 𝐵 ↔ ¬ 𝜑) ⇒ ⊢ (𝜑 ↔ 𝐴 ≠ 𝐵) | ||
Theorem | necon2bbii 3067 | Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.) |
⊢ (𝜑 ↔ 𝐴 ≠ 𝐵) ⇒ ⊢ (𝐴 = 𝐵 ↔ ¬ 𝜑) | ||
Theorem | necon3bii 3068 | Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.) |
⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ⇒ ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) | ||
Theorem | necom 3069 | Commutation of inequality. (Contributed by NM, 14-May-1999.) |
⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) | ||
Theorem | necomi 3070 | Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.) |
⊢ 𝐴 ≠ 𝐵 ⇒ ⊢ 𝐵 ≠ 𝐴 | ||
Theorem | necomd 3071 | Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐴) | ||
Theorem | nesym 3072 | Characterization of inequality in terms of reversed equality (see bicom 223). (Contributed by BJ, 7-Jul-2018.) |
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) | ||
Theorem | nesymi 3073 | Inference associated with nesym 3072. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ 𝐴 ≠ 𝐵 ⇒ ⊢ ¬ 𝐵 = 𝐴 | ||
Theorem | nesymir 3074 | Inference associated with nesym 3072. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ ¬ 𝐴 = 𝐵 ⇒ ⊢ 𝐵 ≠ 𝐴 | ||
Theorem | neeq1d 3075 | Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) | ||
Theorem | neeq2d 3076 | Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) | ||
Theorem | neeq12d 3077 | Deduction for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)) | ||
Theorem | neeq1 3078 | Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) | ||
Theorem | neeq2 3079 | Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) | ||
Theorem | neeq1i 3080 | Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) | ||
Theorem | neeq2i 3081 | Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵) | ||
Theorem | neeq12i 3082 | Inference for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷) | ||
Theorem | eqnetrd 3083 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | eqnetrrd 3084 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐶) | ||
Theorem | neeqtrd 3085 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | eqnetri 3086 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐵 ≠ 𝐶 ⇒ ⊢ 𝐴 ≠ 𝐶 | ||
Theorem | eqnetrri 3087 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐴 ≠ 𝐶 ⇒ ⊢ 𝐵 ≠ 𝐶 | ||
Theorem | neeqtri 3088 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴 ≠ 𝐶 | ||
Theorem | neeqtrri 3089 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴 ≠ 𝐶 | ||
Theorem | neeqtrrd 3090 | Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | eqnetrrid 3091 | A chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | 3netr3d 3092 | 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 3093 | 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 3094 | Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) | ||
Theorem | 3netr4g 3095 | Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) | ||
Theorem | nebi 3096 | Contraposition law for inequality. (Contributed by NM, 28-Dec-2008.) |
⊢ ((𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ↔ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) | ||
Theorem | pm13.18 3097 | 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 3098 | Obsolete version of pm13.18 3097 as of 14-May-2023. (Contributed by Andrew Salmon, 3-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | pm13.181 3099 | Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ≠ 𝐶) → 𝐴 ≠ 𝐶) | ||
Theorem | pm2.61ine 3100 | Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝐴 = 𝐵 → 𝜑) & ⊢ (𝐴 ≠ 𝐵 → 𝜑) ⇒ ⊢ 𝜑 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |