P. 29 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 2801-2900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nfeqd 2801	Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)
Theorem	nfeld 2802	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵)
Theorem	nfnfc 2803	Hypothesis builder for Ⅎ𝑦𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-13 2282. (Revised by Wolf Lammen, 10-Dec-2019.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥Ⅎ𝑦𝐴
Theorem	nfnfcALT 2804	Alternate proof of nfnfc 2803. Shorter but requiring more axioms. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥Ⅎ𝑦𝐴
Theorem	nfeq 2805	Hypothesis builder for equality. (Contributed by NM, 21-Jun-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 = 𝐵
Theorem	nfel 2806	Hypothesis builder for elementhood. (Contributed by NM, 1-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
Theorem	nfeq1 2807*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝐴 = 𝐵
Theorem	nfel1 2808*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
Theorem	nfeq2 2809*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 = 𝐵
Theorem	nfel2 2810*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
Theorem	drnfc1 2811	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑦𝐵))
Theorem	drnfc2 2812	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝐴 ↔ Ⅎ𝑧𝐵))
Theorem	nfabd2 2813	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓})
Theorem	nfabd 2814	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓})
Theorem	dvelimdc 2815	Deduction form of dvelimc 2816. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑧𝐵)    &   ⊢ (𝜑 → (𝑧 = 𝑦 → 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵))
Theorem	dvelimc 2816	Version of dvelim 2368 for classes. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ (𝑧 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵)
Theorem	nfcvf 2817	If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)
Theorem	nfcvf2 2818	If 𝑥 and 𝑦 are distinct, then 𝑦 is not free in 𝑥. (Contributed by Mario Carneiro, 5-Dec-2016.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)
Theorem	cleqf 2819	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqh 2753. (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Nov-2019.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	abid2f 2820	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 2821	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.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑))
Theorem	sbabel 2822*	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.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ([𝑦 / 𝑥]{𝑧 ∣ 𝜑} ∈ 𝐴 ↔ {𝑧 ∣ [𝑦 / 𝑥]𝜑} ∈ 𝐴)
2.1.4  Negated equality and membership
2.1.4.1  Negated equality
Syntax	wne 2823	Extend wff notation to include inequality.
wff 𝐴 ≠ 𝐵
Definition	df-ne 2824	Define inequality. (Contributed by NM, 26-May-1993.)
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
Theorem	neii 2825	Inference associated with df-ne 2824. (Contributed by BJ, 7-Jul-2018.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ ¬ 𝐴 = 𝐵
Theorem	neir 2826	Inference associated with df-ne 2824. (Contributed by BJ, 7-Jul-2018.)
⊢ ¬ 𝐴 = 𝐵    ⇒   ⊢ 𝐴 ≠ 𝐵
Theorem	nne 2827	Negation of inequality. (Contributed by NM, 9-Jun-2006.)
⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
Theorem	neneqd 2828	Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
Theorem	neneq 2829	From inequality to non equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)
Theorem	neqned 2830	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2828. One-way deduction form of df-ne 2824. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2849. (Revised by Wolf Lammen, 22-Nov-2019.)
⊢ (𝜑 → ¬ 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	neqne 2831	From non equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵)
Theorem	neirr 2832	No class is unequal to itself. Inequality is irreflexive. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ ¬ 𝐴 ≠ 𝐴
Theorem	exmidne 2833	Excluded middle with equality and inequality. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 17-Nov-2019.)
⊢ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵)
Theorem	eqneqall 2834	A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑))
Theorem	nonconne 2835	Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 21-Dec-2019.)
⊢ ¬ (𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐵)
Theorem	necon3ad 2836	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 2837	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))    ⇒   ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))
Theorem	necon2ad 2838	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 2839	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
Theorem	necon1ad 2840	Contrapositive deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
Theorem	necon1bd 2841	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 2842	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 2843	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 2844	Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 = 𝐷))    ⇒   ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵))
Theorem	necon1d 2845	Contrapositive law deduction for inequality. (Contributed by NM, 28-Dec-2008.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝐶 = 𝐷))    ⇒   ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵))
Theorem	necon2d 2846	Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 ≠ 𝐷))    ⇒   ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 ≠ 𝐵))
Theorem	necon4d 2847	Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝐶 ≠ 𝐷))    ⇒   ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 = 𝐵))
Theorem	necon3ai 2848	Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑)
Theorem	necon3bi 2849	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 2850	Contrapositive inference for inequality. (Contributed by NM, 12-Feb-2007.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
⊢ (¬ 𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝐴 ≠ 𝐵 → 𝜑)
Theorem	necon1bi 2851	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 2852	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 2853	Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝐴 = 𝐵 → ¬ 𝜑)
Theorem	necon4ai 2854	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 2855	Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷)    ⇒   ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵)
Theorem	necon1i 2856	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
⊢ (𝐴 ≠ 𝐵 → 𝐶 = 𝐷)    ⇒   ⊢ (𝐶 ≠ 𝐷 → 𝐴 = 𝐵)
Theorem	necon2i 2857	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
⊢ (𝐴 = 𝐵 → 𝐶 ≠ 𝐷)    ⇒   ⊢ (𝐶 = 𝐷 → 𝐴 ≠ 𝐵)
Theorem	necon4i 2858	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 2859	Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))
Theorem	necon3bbid 2860	Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))
Theorem	necon1abid 2861	Contrapositive deduction for inequality. (Contributed by NM, 21-Aug-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝜓))
Theorem	necon1bbid 2862	Contrapositive inference for inequality. (Contributed by NM, 31-Jan-2008.)
⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝜓))    ⇒   ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 = 𝐵))
Theorem	necon4abid 2863	Contrapositive law deduction for inequality. (Contributed by NM, 11-Jan-2008.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
Theorem	necon4bbid 2864	Contrapositive law deduction for inequality. (Contributed by NM, 9-May-2012.)
⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵))
Theorem	necon2abid 2865	Contrapositive deduction for inequality. (Contributed by NM, 18-Jul-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵))
Theorem	necon2bbid 2866	Contrapositive deduction for inequality. (Contributed by NM, 13-Apr-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
Theorem	necon3bid 2867	Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))
Theorem	necon4bid 2868	Contrapositive law deduction for inequality. (Contributed by NM, 29-Jun-2007.)
⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))
Theorem	necon3abii 2869	Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
⊢ (𝐴 = 𝐵 ↔ 𝜑)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑)
Theorem	necon3bbii 2870	Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (𝜑 ↔ 𝐴 = 𝐵)    ⇒   ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵)
Theorem	necon1abii 2871	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (¬ 𝜑 ↔ 𝐴 = 𝐵)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ 𝜑)
Theorem	necon1bbii 2872	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
⊢ (𝐴 ≠ 𝐵 ↔ 𝜑)    ⇒   ⊢ (¬ 𝜑 ↔ 𝐴 = 𝐵)
Theorem	necon2abii 2873	Contrapositive inference for inequality. (Contributed by NM, 2-Mar-2007.)
⊢ (𝐴 = 𝐵 ↔ ¬ 𝜑)    ⇒   ⊢ (𝜑 ↔ 𝐴 ≠ 𝐵)
Theorem	necon2bbii 2874	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (𝜑 ↔ 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝐴 = 𝐵 ↔ ¬ 𝜑)
Theorem	necon3bii 2875	Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)
Theorem	necom 2876	Commutation of inequality. (Contributed by NM, 14-May-1999.)
⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
Theorem	necomi 2877	Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ 𝐵 ≠ 𝐴
Theorem	necomd 2878	Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐴)
Theorem	nesym 2879	Characterization of inequality in terms of reversed equality (see bicom 212). (Contributed by BJ, 7-Jul-2018.)
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)
Theorem	nesymi 2880	Inference associated with nesym 2879. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ ¬ 𝐵 = 𝐴
Theorem	nesymir 2881	Inference associated with nesym 2879. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ ¬ 𝐴 = 𝐵    ⇒   ⊢ 𝐵 ≠ 𝐴
Theorem	neeq1d 2882	Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
Theorem	neeq2d 2883	Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
Theorem	neeq12d 2884	Deduction for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷))
Theorem	neeq1 2885	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
Theorem	neeq2 2886	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
Theorem	neeq1i 2887	Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)
Theorem	neeq2i 2888	Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)
Theorem	neeq12i 2889	Inference for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)
Theorem	eqnetrd 2890	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	eqnetrrd 2891	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐶)
Theorem	neeqtrd 2892	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	eqnetri 2893	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 ≠ 𝐶    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	eqnetrri 2894	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 ≠ 𝐶    ⇒   ⊢ 𝐵 ≠ 𝐶
Theorem	neeqtri 2895	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	neeqtrri 2896	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	neeqtrrd 2897	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	syl5eqner 2898	A chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	3netr3d 2899	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 2900	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 21-Nov-2019.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)