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