P. 24 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2301-2400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	abeq1i 2301	Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 31-Jul-1994.)
⊢ {𝑥 ∣ 𝜑} = 𝐴    ⇒   ⊢ (𝜑 ↔ 𝑥 ∈ 𝐴)
Theorem	abeq2d 2302	Equality of a class variable and a class abstraction (deduction). (Contributed by NM, 16-Nov-1995.)
⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))
Theorem	abbi 2303	Equivalent wff's correspond to equal class abstractions. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
Theorem	abbi2i 2304*	Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 5-Aug-1993.)
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)    ⇒   ⊢ 𝐴 = {𝑥 ∣ 𝜑}
Theorem	abbii 2305	Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}
Theorem	abbid 2306	Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
Theorem	abbidv 2307*	Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
Theorem	abbi2dv 2308*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))    ⇒   ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})
Theorem	abbi1dv 2309*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴)
Theorem	abid2 2310*	A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.)
⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴
Theorem	sb8ab 2311	Substitution of variable in class abstraction. (Contributed by Jim Kingdon, 27-Sep-2018.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ [𝑦 / 𝑥]𝜑}
Theorem	cbvabw 2312*	Version of cbvab 2313 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
Theorem	cbvab 2313	Rule used to change bound variables, using implicit substitution. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
Theorem	cbvabv 2314*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
Theorem	clelab 2315*	Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993.)
⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
Theorem	clabel 2316*	Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006.)
⊢ ({𝑥 ∣ 𝜑} ∈ 𝐴 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑)))
Theorem	sbab 2317*	The right-hand side of the second equality is a way of representing proper substitution of 𝑦 for 𝑥 into a class variable. (Contributed by NM, 14-Sep-2003.)
⊢ (𝑥 = 𝑦 → 𝐴 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐴})
2.1.2.1  Elementary properties of class abstractions
Theorem	eqabdv 2318*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) (Revised by Wolf Lammen, 6-May-2023.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))    ⇒   ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})
2.1.3  Class form not-free predicate
Syntax	wnfc 2319	Extend wff definition to include the not-free predicate for classes.
wff Ⅎ𝑥𝐴
Theorem	nfcjust 2320*	Justification theorem for df-nfc 2321. (Contributed by Mario Carneiro, 13-Oct-2016.)
⊢ (∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴 ↔ ∀𝑧Ⅎ𝑥 𝑧 ∈ 𝐴)
Definition	df-nfc 2321*	Define the not-free predicate for classes. This is read "𝑥 is not free in 𝐴". Not-free means that the value of 𝑥 cannot affect the value of 𝐴, e.g., any occurrence of 𝑥 in 𝐴 is effectively bound by a quantifier or something that expands to one (such as "there exists at most one"). It is defined in terms of the not-free predicate df-nf 1472 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	nfci 2322*	Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥 𝑦 ∈ 𝐴    ⇒   ⊢ Ⅎ𝑥𝐴
Theorem	nfcii 2323*	Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ Ⅎ𝑥𝐴
Theorem	nfcr 2324*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	nfcrii 2325*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
Theorem	nfcri 2326*	Consequence of the not-free predicate. (Note that unlike nfcr 2324, this does not require 𝑦 and 𝐴 to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
Theorem	nfcd 2327*	Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐴)
Theorem	nfceqi 2328	Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)
Theorem	nfcxfr 2329	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ 𝐴 = 𝐵    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥𝐴
Theorem	nfcxfrd 2330	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐴)
Theorem	nfceqdf 2331	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵))
Theorem	nfcv 2332*	If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴
Theorem	nfcvd 2333*	If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)
Theorem	nfab1 2334	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}
Theorem	nfnfc1 2335	𝑥 is bound in Ⅎ𝑥𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥Ⅎ𝑥𝐴
Theorem	clelsb1f 2336	Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2167). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
Theorem	nfab 2337	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}
Theorem	nfaba1 2338	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥𝜑}
Theorem	nfnfc 2339	Hypothesis builder for Ⅎ𝑦𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥Ⅎ𝑦𝐴
Theorem	nfeq 2340	Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 = 𝐵
Theorem	nfel 2341	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
Theorem	nfeq1 2342*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝐴 = 𝐵
Theorem	nfel1 2343*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
Theorem	nfeq2 2344*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 = 𝐵
Theorem	nfel2 2345*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
Theorem	nfcrd 2346*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	nfeqd 2347	Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)
Theorem	nfeld 2348	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵)
Theorem	drnfc1 2349	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑦𝐵))
Theorem	drnfc2 2350	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝐴 ↔ Ⅎ𝑧𝐵))
Theorem	nfabdw 2351*	Bound-variable hypothesis builder for a class abstraction. Version of nfabd 2352 with a disjoint variable condition. (Contributed by Mario Carneiro, 8-Oct-2016.) (Revised by Gino Giotto, 10-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓})
Theorem	nfabd 2352	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓})
Theorem	dvelimdc 2353	Deduction form of dvelimc 2354. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑧𝐵)    &   ⊢ (𝜑 → (𝑧 = 𝑦 → 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵))
Theorem	dvelimc 2354	Version of dvelim 2029 for classes. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ (𝑧 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵)
Theorem	nfcvf 2355	If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)
Theorem	nfcvf2 2356	If 𝑥 and 𝑦 are distinct, then 𝑦 is not free in 𝑥. (Contributed by Mario Carneiro, 5-Dec-2016.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)
Theorem	cleqf 2357	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqh 2289. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	abid2f 2358	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.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴
Theorem	sbabel 2359*	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.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ([𝑦 / 𝑥]{𝑧 ∣ 𝜑} ∈ 𝐴 ↔ {𝑧 ∣ [𝑦 / 𝑥]𝜑} ∈ 𝐴)
2.1.4  Negated equality and membership
2.1.4.1  Negated equality
Syntax	wne 2360	Extend wff notation to include inequality.
wff 𝐴 ≠ 𝐵
Definition	df-ne 2361	Define inequality. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
Theorem	neii 2362	Inference associated with df-ne 2361. (Contributed by BJ, 7-Jul-2018.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ ¬ 𝐴 = 𝐵
Theorem	neir 2363	Inference associated with df-ne 2361. (Contributed by BJ, 7-Jul-2018.)
⊢ ¬ 𝐴 = 𝐵    ⇒   ⊢ 𝐴 ≠ 𝐵
Theorem	nner 2364	Negation of inequality. (Contributed by Jim Kingdon, 23-Dec-2018.)
⊢ (𝐴 = 𝐵 → ¬ 𝐴 ≠ 𝐵)
Theorem	nnedc 2365	Negation of inequality where equality is decidable. (Contributed by Jim Kingdon, 15-May-2018.)
⊢ (DECID 𝐴 = 𝐵 → (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	dcned 2366	Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.)
⊢ (𝜑 → DECID 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → DECID 𝐴 ≠ 𝐵)
Theorem	neqned 2367	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2381. One-way deduction form of df-ne 2361. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2410. (Revised by Wolf Lammen, 22-Nov-2019.)
⊢ (𝜑 → ¬ 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	neqne 2368	From non-equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵)
Theorem	neirr 2369	No class is unequal to itself. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ ¬ 𝐴 ≠ 𝐴
Theorem	eqneqall 2370	A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑))
Theorem	dcne 2371	Decidable equality expressed in terms of ≠. Basically the same as df-dc 836. (Contributed by Jim Kingdon, 14-Mar-2020.)
⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵))
Theorem	nonconne 2372	Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.)
⊢ ¬ (𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐵)
Theorem	neeq1 2373	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
Theorem	neeq2 2374	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
Theorem	neeq1i 2375	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)
Theorem	neeq2i 2376	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)
Theorem	neeq12i 2377	Inference for inequality. (Contributed by NM, 24-Jul-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)
Theorem	neeq1d 2378	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
Theorem	neeq2d 2379	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
Theorem	neeq12d 2380	Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷))
Theorem	neneqd 2381	Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
Theorem	neneq 2382	From inequality to non-equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)
Theorem	eqnetri 2383	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 ≠ 𝐶    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	eqnetrd 2384	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	eqnetrri 2385	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 ≠ 𝐶    ⇒   ⊢ 𝐵 ≠ 𝐶
Theorem	eqnetrrd 2386	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐶)
Theorem	neeqtri 2387	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	neeqtrd 2388	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	neeqtrri 2389	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	neeqtrrd 2390	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	eqnetrrid 2391	B chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	3netr3d 2392	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	3netr4d 2393	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	3netr3g 2394	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	3netr4g 2395	Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	necon3abii 2396	Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
⊢ (𝐴 = 𝐵 ↔ 𝜑)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑)
Theorem	necon3bbii 2397	Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (𝜑 ↔ 𝐴 = 𝐵)    ⇒   ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵)
Theorem	necon3bii 2398	Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)
Theorem	necon3abid 2399	Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))
Theorem	necon3bbid 2400	Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))