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	eqeltrrdi 2301	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ (𝜑 → 𝐵 = 𝐴)    &   ⊢ 𝐵 ∈ 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eleqtrdi 2302	A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eleqtrrdi 2303	A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	eleq2s 2304	Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝐴 ∈ 𝐵 → 𝜑)    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ (𝐴 ∈ 𝐶 → 𝜑)
Theorem	eqneltrd 2305	If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)
Theorem	eqneltrrd 2306	If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐶)
Theorem	neleqtrd 2307	If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵)
Theorem	neleqtrrd 2308	If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴)
Theorem	cleqh 2309*	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqf 2377. (Contributed by NM, 5-Aug-1993.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    &   ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵)    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	nelneq 2310	A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997.)
⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵)
Theorem	nelneq2 2311	A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002.)
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 = 𝐶)
Theorem	eqsb1lem 2312*	Lemma for eqsb1 2313. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ ([𝑦 / 𝑥]𝑥 = 𝐴 ↔ 𝑦 = 𝐴)
Theorem	eqsb1 2313*	Substitution for the left-hand side in an equality. Class version of equsb3 1982. (Contributed by Rodolfo Medina, 28-Apr-2010.)
⊢ ([𝑦 / 𝑥]𝑥 = 𝐴 ↔ 𝑦 = 𝐴)
Theorem	clelsb1 2314*	Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2187). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
Theorem	clelsb2 2315*	Substitution for the second argument of the membership predicate in an atomic formula (class version of elsb2 2188). (Contributed by Jim Kingdon, 22-Nov-2018.)
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)
Theorem	hbxfreq 2316	A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1498 for equivalence version. (Contributed by NM, 21-Aug-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵)    ⇒   ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
Theorem	hblem 2317*	Change the free variable of a hypothesis builder. (Contributed by NM, 5-Aug-1993.) (Revised by Andrew Salmon, 11-Jul-2011.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ (𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴)
Theorem	abeq2 2318*	Equality of a class variable and a class abstraction (also called a class builder). Theorem 5.1 of [Quine] p. 34. This theorem shows the relationship between expressions with class abstractions and expressions with class variables. Note that abbi 2323 and its relatives are among those useful for converting theorems with class variables to equivalent theorems with wff variables, by first substituting a class abstraction for each class variable. Class variables can always be eliminated from a theorem to result in an equivalent theorem with wff variables, and vice-versa. The idea is roughly as follows. To convert a theorem with a wff variable 𝜑 (that has a free variable 𝑥) to a theorem with a class variable 𝐴, we substitute 𝑥 ∈ 𝐴 for 𝜑 throughout and simplify, where 𝐴 is a new class variable not already in the wff. Conversely, to convert a theorem with a class variable 𝐴 to one with 𝜑, we substitute {𝑥 ∣ 𝜑} for 𝐴 throughout and simplify, where 𝑥 and 𝜑 are new set and wff variables not already in the wff. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑))
Theorem	abeq1 2319*	Equality of a class variable and a class abstraction. (Contributed by NM, 20-Aug-1993.)
⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝜑 ↔ 𝑥 ∈ 𝐴))
Theorem	abeq2i 2320	Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.)
⊢ 𝐴 = {𝑥 ∣ 𝜑}    ⇒   ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)
Theorem	abeq1i 2321	Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 31-Jul-1994.)
⊢ {𝑥 ∣ 𝜑} = 𝐴    ⇒   ⊢ (𝜑 ↔ 𝑥 ∈ 𝐴)
Theorem	abeq2d 2322	Equality of a class variable and a class abstraction (deduction). (Contributed by NM, 16-Nov-1995.)
⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))
Theorem	abbi 2323	Equivalent wff's correspond to equal class abstractions. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
Theorem	abbi2i 2324*	Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 5-Aug-1993.)
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)    ⇒   ⊢ 𝐴 = {𝑥 ∣ 𝜑}
Theorem	abbii 2325	Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}
Theorem	abbid 2326	Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
Theorem	abbidv 2327*	Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
Theorem	abbi2dv 2328*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))    ⇒   ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})
Theorem	abbi1dv 2329*	Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴)
Theorem	abid2 2330*	A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.)
⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴
Theorem	sb8ab 2331	Substitution of variable in class abstraction. (Contributed by Jim Kingdon, 27-Sep-2018.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ [𝑦 / 𝑥]𝜑}
Theorem	cbvabw 2332*	Version of cbvab 2333 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
Theorem	cbvab 2333	Rule used to change bound variables, using implicit substitution. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
Theorem	cbvabv 2334*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
Theorem	clelab 2335*	Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993.)
⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
Theorem	clabel 2336*	Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006.)
⊢ ({𝑥 ∣ 𝜑} ∈ 𝐴 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑)))
Theorem	sbab 2337*	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 2338*	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 2339	Extend wff definition to include the not-free predicate for classes.
wff Ⅎ𝑥𝐴
Theorem	nfcjust 2340*	Justification theorem for df-nfc 2341. (Contributed by Mario Carneiro, 13-Oct-2016.)
⊢ (∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴 ↔ ∀𝑧Ⅎ𝑥 𝑧 ∈ 𝐴)
Definition	df-nfc 2341*	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 1487 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	nfci 2342*	Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥 𝑦 ∈ 𝐴    ⇒   ⊢ Ⅎ𝑥𝐴
Theorem	nfcii 2343*	Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ Ⅎ𝑥𝐴
Theorem	nfcr 2344*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	nfcrii 2345*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
Theorem	nfcri 2346*	Consequence of the not-free predicate. (Note that unlike nfcr 2344, this does not require 𝑦 and 𝐴 to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
Theorem	nfcd 2347*	Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐴)
Theorem	nfceqi 2348	Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)
Theorem	nfcxfr 2349	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ 𝐴 = 𝐵    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥𝐴
Theorem	nfcxfrd 2350	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐴)
Theorem	nfceqdf 2351	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵))
Theorem	nfcv 2352*	If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴
Theorem	nfcvd 2353*	If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)
Theorem	nfab1 2354	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}
Theorem	nfnfc1 2355	𝑥 is bound in Ⅎ𝑥𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥Ⅎ𝑥𝐴
Theorem	clelsb1f 2356	Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2187). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
Theorem	nfab 2357	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}
Theorem	nfaba1 2358	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥𝜑}
Theorem	nfnfc 2359	Hypothesis builder for Ⅎ𝑦𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥Ⅎ𝑦𝐴
Theorem	nfeq 2360	Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 = 𝐵
Theorem	nfel 2361	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
Theorem	nfeq1 2362*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝐴 = 𝐵
Theorem	nfel1 2363*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
Theorem	nfeq2 2364*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 = 𝐵
Theorem	nfel2 2365*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
Theorem	nfcrd 2366*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	nfeqd 2367	Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)
Theorem	nfeld 2368	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵)
Theorem	drnfc1 2369	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑦𝐵))
Theorem	drnfc2 2370	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝐴 ↔ Ⅎ𝑧𝐵))
Theorem	nfabdw 2371*	Bound-variable hypothesis builder for a class abstraction. Version of nfabd 2372 with a disjoint variable condition. (Contributed by Mario Carneiro, 8-Oct-2016.) (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓})
Theorem	nfabd 2372	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓})
Theorem	dvelimdc 2373	Deduction form of dvelimc 2374. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑧𝐵)    &   ⊢ (𝜑 → (𝑧 = 𝑦 → 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵))
Theorem	dvelimc 2374	Version of dvelim 2048 for classes. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ (𝑧 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵)
Theorem	nfcvf 2375	If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)
Theorem	nfcvf2 2376	If 𝑥 and 𝑦 are distinct, then 𝑦 is not free in 𝑥. (Contributed by Mario Carneiro, 5-Dec-2016.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)
Theorem	cleqf 2377	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqh 2309. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	abid2f 2378	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 2379*	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 2380	Extend wff notation to include inequality.
wff 𝐴 ≠ 𝐵
Definition	df-ne 2381	Define inequality. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
Theorem	neii 2382	Inference associated with df-ne 2381. (Contributed by BJ, 7-Jul-2018.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ ¬ 𝐴 = 𝐵
Theorem	neir 2383	Inference associated with df-ne 2381. (Contributed by BJ, 7-Jul-2018.)
⊢ ¬ 𝐴 = 𝐵    ⇒   ⊢ 𝐴 ≠ 𝐵
Theorem	nner 2384	Negation of inequality. (Contributed by Jim Kingdon, 23-Dec-2018.)
⊢ (𝐴 = 𝐵 → ¬ 𝐴 ≠ 𝐵)
Theorem	nnedc 2385	Negation of inequality where equality is decidable. (Contributed by Jim Kingdon, 15-May-2018.)
⊢ (DECID 𝐴 = 𝐵 → (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	dcned 2386	Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.)
⊢ (𝜑 → DECID 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → DECID 𝐴 ≠ 𝐵)
Theorem	neqned 2387	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2401. One-way deduction form of df-ne 2381. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2430. (Revised by Wolf Lammen, 22-Nov-2019.)
⊢ (𝜑 → ¬ 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	neqne 2388	From non-equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵)
Theorem	neirr 2389	No class is unequal to itself. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ ¬ 𝐴 ≠ 𝐴
Theorem	eqneqall 2390	A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑))
Theorem	dcne 2391	Decidable equality expressed in terms of ≠. Basically the same as df-dc 839. (Contributed by Jim Kingdon, 14-Mar-2020.)
⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵))
Theorem	nonconne 2392	Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.)
⊢ ¬ (𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐵)
Theorem	neeq1 2393	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
Theorem	neeq2 2394	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
Theorem	neeq1i 2395	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)
Theorem	neeq2i 2396	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)
Theorem	neeq12i 2397	Inference for inequality. (Contributed by NM, 24-Jul-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)
Theorem	neeq1d 2398	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
Theorem	neeq2d 2399	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
Theorem	neeq12d 2400	Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷))