P. 30 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 2901-3000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nfcxfrd 2901	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐴)
Theorem	nfcv 2902*	If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴
Theorem	nfcvd 2903*	If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)
Theorem	nfab1 2904	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}
Theorem	nfnfc1 2905	The setvar 𝑥 is bound in Ⅎ𝑥𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥Ⅎ𝑥𝐴
Theorem	clelsb1fw 2906*	Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2113). Version of clelsb1f 2907 with a disjoint variable condition, which does not require ax-13 2374. (Contributed by Rodolfo Medina, 28-Apr-2010.) Avoid ax-13 2374. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
Theorem	clelsb1f 2907	Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2113). Usage of this theorem is discouraged because it depends on ax-13 2374. See clelsb1fw 2906 not requiring ax-13 2374, but extra disjoint variables. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.) (Proof shortened by Wolf Lammen, 7-May-2023.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
Theorem	nfab 2908*	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Add disjoint variable condition to avoid ax-13 2374. See nfabg 2909 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}
Theorem	nfabg 2909	Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2374. See nfab 2908 for a version with more disjoint variable conditions, but not requiring ax-13 2374. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}
Theorem	nfaba1 2910*	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.) Add disjoint variable condition to avoid ax-13 2374. See nfaba1g 2912 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.) Avoid ax-6 1964, ax-7 2004, ax-12 2174. (Revised by SN, 14-May-2025.)
⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥𝜑}
Theorem	nfaba1OLD 2911*	Obsolete version of nfaba1 2910 as of 14-May-2025. (Contributed by Mario Carneiro, 14-Oct-2016.) (Revised by GG, 20-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥𝜑}
Theorem	nfaba1g 2912	Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2374. See nfaba1 2910 for a version with a disjoint variable condition, but not requiring ax-13 2374. (Contributed by Mario Carneiro, 14-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥𝜑}
Theorem	nfeqd 2913	Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)
Theorem	nfeld 2914	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵)
Theorem	nfnfc 2915	Hypothesis builder for Ⅎ𝑦𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-13 2374. (Revised by Wolf Lammen, 10-Dec-2019.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥Ⅎ𝑦𝐴
Theorem	nfeq 2916	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 2917	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 2918*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝐴 = 𝐵
Theorem	nfel1 2919*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
Theorem	nfeq2 2920*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 = 𝐵
Theorem	nfel2 2921*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
Theorem	drnfc1 2922	Formula-building lemma for use with the Distinctor Reduction Theorem. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by Mario Carneiro, 8-Oct-2016.) Avoid ax-8 2107, ax-11 2154. (Revised by Wolf Lammen, 22-Sep-2024.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑦𝐵))
Theorem	drnfc2 2923	Formula-building lemma for use with the Distinctor Reduction Theorem. Proof revision is marked as discouraged because the minimizer replaces albidv 1917 with dral2 2440, leading to a one byte longer proof. However feel free to manually edit it according to conventions. (TODO: dral2 2440 depends on ax-13 2374, hence its usage during minimizing is discouraged. Check in the long run whether this is a permanent restriction). Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by Mario Carneiro, 8-Oct-2016.) Avoid ax-8 2107. (Revised by Wolf Lammen, 22-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝐴 ↔ Ⅎ𝑧𝐵))
Theorem	nfabdw 2924*	Bound-variable hypothesis builder for a class abstraction. Version of nfabd 2925 with a disjoint variable condition, which does not require ax-13 2374. (Contributed by Mario Carneiro, 8-Oct-2016.) Avoid ax-13 2374. (Revised by GG, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 23-Sep-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓})
Theorem	nfabd 2925	Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2374. Use the weaker nfabdw 2924 when possible. (Contributed by Mario Carneiro, 8-Oct-2016.) Avoid ax-9 2115 and ax-ext 2705. (Revised by Wolf Lammen, 23-May-2023.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓})
Theorem	nfabd2 2926	Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by Mario Carneiro, 8-Oct-2016.) (Proof shortened by Wolf Lammen, 10-May-2023.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓})
Theorem	dvelimdc 2927	Deduction form of dvelimc 2928. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by Mario Carneiro, 8-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑧𝐵)    &   ⊢ (𝜑 → (𝑧 = 𝑦 → 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵))
Theorem	dvelimc 2928	Version of dvelim 2453 for classes. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by Mario Carneiro, 8-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ (𝑧 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵)
Theorem	nfcvf 2929	If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2374. See nfcv 2902 for a version that replaces the distinctor with a disjoint variable condition, requiring fewer axioms. (Contributed by Mario Carneiro, 8-Oct-2016.) Avoid ax-ext 2705. (Revised by Wolf Lammen, 10-May-2023.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)
Theorem	nfcvf2 2930	If 𝑥 and 𝑦 are distinct, then 𝑦 is not free in 𝑥. Usage of this theorem is discouraged because it depends on ax-13 2374. See nfcv 2902 for a version that replaces the distinctor with a disjoint variable condition, requiring fewer axioms. (Contributed by Mario Carneiro, 5-Dec-2016.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)
Theorem	cleqf 2931	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions as in dfcleq 2727. See also cleqh 2868. (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Nov-2019.) Avoid ax-13 2374. (Revised by Wolf Lammen, 10-May-2023.) Avoid ax-10 2138. (Revised by GG, 20-Aug-2023.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	eqabf 2932	Equality of a class variable and a class abstraction. In this version, the fact that 𝑥 is a nonfree variable in 𝐴 is explicitly stated as a hypothesis. (Contributed by Thierry Arnoux, 11-May-2017.) Avoid ax-13 2374. (Revised by Wolf Lammen, 13-May-2023.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑))
Theorem	abid2f 2933	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, 26-Feb-2025.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴
Theorem	abid2fOLD 2934	Obsolete version of abid2f 2933 as of 26-Feb-2025. (Contributed by NM, 5-Sep-2011.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴
Theorem	sbabel 2935*	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, 28-Oct-2024.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ([𝑦 / 𝑥]{𝑧 ∣ 𝜑} ∈ 𝐴 ↔ {𝑧 ∣ [𝑦 / 𝑥]𝜑} ∈ 𝐴)
Theorem	sbabelOLD 2936*	Obsolete version of sbabel 2935 as of 28-Oct-2024. (Contributed by NM, 27-Sep-2003.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 26-Dec-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ([𝑦 / 𝑥]{𝑧 ∣ 𝜑} ∈ 𝐴 ↔ {𝑧 ∣ [𝑦 / 𝑥]𝜑} ∈ 𝐴)
2.1.4  Negated equality and membership
2.1.4.1  Negated equality
Syntax	wne 2937	Extend wff notation to include inequality.
wff 𝐴 ≠ 𝐵
Definition	df-ne 2938	Define inequality. (Contributed by NM, 26-May-1993.)
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
Theorem	neii 2939	Inference associated with df-ne 2938. (Contributed by BJ, 7-Jul-2018.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ ¬ 𝐴 = 𝐵
Theorem	neir 2940	Inference associated with df-ne 2938. (Contributed by BJ, 7-Jul-2018.)
⊢ ¬ 𝐴 = 𝐵    ⇒   ⊢ 𝐴 ≠ 𝐵
Theorem	nne 2941	Negation of inequality. (Contributed by NM, 9-Jun-2006.)
⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
Theorem	neneqd 2942	Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
Theorem	neneq 2943	From inequality to non-equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)
Theorem	neqned 2944	If it is not the case that two classes are equal, then they are unequal. Converse of neneqd 2942. One-way deduction form of df-ne 2938. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2964. (Revised by Wolf Lammen, 22-Nov-2019.)
⊢ (𝜑 → ¬ 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	neqne 2945	From non-equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵)
Theorem	neirr 2946	No class is unequal to itself. Inequality is irreflexive. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ ¬ 𝐴 ≠ 𝐴
Theorem	exmidne 2947	Excluded middle with equality and inequality. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 17-Nov-2019.)
⊢ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵)
Theorem	eqneqall 2948	A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑))
Theorem	nonconne 2949	Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 21-Dec-2019.)
⊢ ¬ (𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐵)
Theorem	necon3ad 2950	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 2951	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))    ⇒   ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))
Theorem	necon2ad 2952	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 2953	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
Theorem	necon1ad 2954	Contrapositive deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
Theorem	necon1bd 2955	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 2956	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 2957	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 2958	Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 = 𝐷))    ⇒   ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵))
Theorem	necon1d 2959	Contrapositive law deduction for inequality. (Contributed by NM, 28-Dec-2008.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝐶 = 𝐷))    ⇒   ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵))
Theorem	necon2d 2960	Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 ≠ 𝐷))    ⇒   ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 ≠ 𝐵))
Theorem	necon4d 2961	Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝐶 ≠ 𝐷))    ⇒   ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 = 𝐵))
Theorem	necon3ai 2962	Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 28-Oct-2024.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑)
Theorem	necon3aiOLD 2963	Obsolete version of necon3ai 2962 as of 28-Oct-2024. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑)
Theorem	necon3bi 2964	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 2965	Contrapositive inference for inequality. (Contributed by NM, 12-Feb-2007.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
⊢ (¬ 𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝐴 ≠ 𝐵 → 𝜑)
Theorem	necon1bi 2966	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 2967	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 2968	Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝐴 = 𝐵 → ¬ 𝜑)
Theorem	necon4ai 2969	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 2970	Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷)    ⇒   ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵)
Theorem	necon1i 2971	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
⊢ (𝐴 ≠ 𝐵 → 𝐶 = 𝐷)    ⇒   ⊢ (𝐶 ≠ 𝐷 → 𝐴 = 𝐵)
Theorem	necon2i 2972	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
⊢ (𝐴 = 𝐵 → 𝐶 ≠ 𝐷)    ⇒   ⊢ (𝐶 = 𝐷 → 𝐴 ≠ 𝐵)
Theorem	necon4i 2973	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 2974	Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))
Theorem	necon3bbid 2975	Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))
Theorem	necon1abid 2976	Contrapositive deduction for inequality. (Contributed by NM, 21-Aug-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝜓))
Theorem	necon1bbid 2977	Contrapositive inference for inequality. (Contributed by NM, 31-Jan-2008.)
⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝜓))    ⇒   ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 = 𝐵))
Theorem	necon4abid 2978	Contrapositive law deduction for inequality. (Contributed by NM, 11-Jan-2008.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
Theorem	necon4bbid 2979	Contrapositive law deduction for inequality. (Contributed by NM, 9-May-2012.)
⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵))
Theorem	necon2abid 2980	Contrapositive deduction for inequality. (Contributed by NM, 18-Jul-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵))
Theorem	necon2bbid 2981	Contrapositive deduction for inequality. (Contributed by NM, 13-Apr-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
Theorem	necon3bid 2982	Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))
Theorem	necon4bid 2983	Contrapositive law deduction for inequality. (Contributed by NM, 29-Jun-2007.)
⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))
Theorem	necon3abii 2984	Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
⊢ (𝐴 = 𝐵 ↔ 𝜑)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑)
Theorem	necon3bbii 2985	Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (𝜑 ↔ 𝐴 = 𝐵)    ⇒   ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵)
Theorem	necon1abii 2986	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (¬ 𝜑 ↔ 𝐴 = 𝐵)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ 𝜑)
Theorem	necon1bbii 2987	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
⊢ (𝐴 ≠ 𝐵 ↔ 𝜑)    ⇒   ⊢ (¬ 𝜑 ↔ 𝐴 = 𝐵)
Theorem	necon2abii 2988	Contrapositive inference for inequality. (Contributed by NM, 2-Mar-2007.)
⊢ (𝐴 = 𝐵 ↔ ¬ 𝜑)    ⇒   ⊢ (𝜑 ↔ 𝐴 ≠ 𝐵)
Theorem	necon2bbii 2989	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (𝜑 ↔ 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝐴 = 𝐵 ↔ ¬ 𝜑)
Theorem	necon3bii 2990	Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)
Theorem	necom 2991	Commutation of inequality. (Contributed by NM, 14-May-1999.)
⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
Theorem	necomi 2992	Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ 𝐵 ≠ 𝐴
Theorem	necomd 2993	Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐴)
Theorem	nesym 2994	Characterization of inequality in terms of reversed equality (see bicom 222). (Contributed by BJ, 7-Jul-2018.)
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)
Theorem	nesymi 2995	Inference associated with nesym 2994. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ ¬ 𝐵 = 𝐴
Theorem	nesymir 2996	Inference associated with nesym 2994. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ ¬ 𝐴 = 𝐵    ⇒   ⊢ 𝐵 ≠ 𝐴
Theorem	neeq1d 2997	Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
Theorem	neeq2d 2998	Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
Theorem	neeq12d 2999	Deduction for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷))
Theorem	neeq1 3000	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))