P. 23 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2201-2300   *Has distinct variable group(s)

Type	Label	Description
Statement
2.1.4  Negated equality and membership
Syntax	wne 2201	Extend wff notation to include inequality.
wff A ≠ B
Syntax	wnel 2202	Extend wff notation to include negated membership.
wff A ∉ B
Definition	df-ne 2203	Define inequality. (Contributed by NM, 5-Aug-1993.)
⊢ (A ≠ B ↔ ¬ A = B)
Definition	df-nel 2204	Define negated membership. (Contributed by NM, 7-Aug-1994.)
⊢ (A ∉ B ↔ ¬ A ∈ B)
2.1.4.1  Negated equality
Theorem	neii 2205	Inference associated with df-ne 2203. (Contributed by BJ, 7-Jul-2018.)
⊢ A ≠ B    ⇒   ⊢ ¬ A = B
Theorem	neir 2206	Inference associated with df-ne 2203. (Contributed by BJ, 7-Jul-2018.)
⊢ ¬ A = B    ⇒   ⊢ A ≠ B
Theorem	nner 2207	Negation of inequality. (Contributed by Jim Kingdon, 23-Dec-2018.)
⊢ (A = B → ¬ A ≠ B)
Theorem	nnedc 2208	Negation of inequality where equality is decidable. (Contributed by Jim Kingdon, 15-May-2018.)
⊢ (DECID A = B → (¬ A ≠ B ↔ A = B))
Theorem	dcned 2209	Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.)
⊢ (φ → DECID A = B)    ⇒   ⊢ (φ → DECID A ≠ B)
Theorem	neirr 2210	No class is unequal to itself. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ ¬ A ≠ A
Theorem	dcne 2211	Decidable equality expressed in terms of ≠. Basically the same as df-dc 742. (Contributed by Jim Kingdon, 14-Mar-2020.)
⊢ (DECID A = B ↔ (A = B ∨ A ≠ B))
Theorem	nonconne 2212	Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.)
⊢ ¬ (A = B ∧ A ≠ B)
Theorem	neeq1 2213	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
⊢ (A = B → (A ≠ 𝐶 ↔ B ≠ 𝐶))
Theorem	neeq2 2214	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
⊢ (A = B → (𝐶 ≠ A ↔ 𝐶 ≠ B))
Theorem	neeq1i 2215	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
⊢ A = B    ⇒   ⊢ (A ≠ 𝐶 ↔ B ≠ 𝐶)
Theorem	neeq2i 2216	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
⊢ A = B    ⇒   ⊢ (𝐶 ≠ A ↔ 𝐶 ≠ B)
Theorem	neeq12i 2217	Inference for inequality. (Contributed by NM, 24-Jul-2012.)
⊢ A = B    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (A ≠ 𝐶 ↔ B ≠ 𝐷)
Theorem	neeq1d 2218	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ≠ 𝐶 ↔ B ≠ 𝐶))
Theorem	neeq2d 2219	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (𝐶 ≠ A ↔ 𝐶 ≠ B))
Theorem	neeq12d 2220	Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (φ → A = B)    &   ⊢ (φ → 𝐶 = 𝐷)    ⇒   ⊢ (φ → (A ≠ 𝐶 ↔ B ≠ 𝐷))
Theorem	neneqd 2221	Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (φ → A ≠ B)    ⇒   ⊢ (φ → ¬ A = B)
Theorem	eqnetri 2222	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ A = B    &   ⊢ B ≠ 𝐶    ⇒   ⊢ A ≠ 𝐶
Theorem	eqnetrd 2223	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (φ → A = B)    &   ⊢ (φ → B ≠ 𝐶)    ⇒   ⊢ (φ → A ≠ 𝐶)
Theorem	eqnetrri 2224	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ A = B    &   ⊢ A ≠ 𝐶    ⇒   ⊢ B ≠ 𝐶
Theorem	eqnetrrd 2225	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (φ → A = B)    &   ⊢ (φ → A ≠ 𝐶)    ⇒   ⊢ (φ → B ≠ 𝐶)
Theorem	neeqtri 2226	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ A ≠ B    &   ⊢ B = 𝐶    ⇒   ⊢ A ≠ 𝐶
Theorem	neeqtrd 2227	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (φ → A ≠ B)    &   ⊢ (φ → B = 𝐶)    ⇒   ⊢ (φ → A ≠ 𝐶)
Theorem	neeqtrri 2228	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ A ≠ B    &   ⊢ 𝐶 = B    ⇒   ⊢ A ≠ 𝐶
Theorem	neeqtrrd 2229	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (φ → A ≠ B)    &   ⊢ (φ → 𝐶 = B)    ⇒   ⊢ (φ → A ≠ 𝐶)
Theorem	syl5eqner 2230	B chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.)
⊢ B = A    &   ⊢ (φ → B ≠ 𝐶)    ⇒   ⊢ (φ → A ≠ 𝐶)
Theorem	3netr3d 2231	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (φ → A ≠ B)    &   ⊢ (φ → A = 𝐶)    &   ⊢ (φ → B = 𝐷)    ⇒   ⊢ (φ → 𝐶 ≠ 𝐷)
Theorem	3netr4d 2232	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (φ → A ≠ B)    &   ⊢ (φ → 𝐶 = A)    &   ⊢ (φ → 𝐷 = B)    ⇒   ⊢ (φ → 𝐶 ≠ 𝐷)
Theorem	3netr3g 2233	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (φ → A ≠ B)    &   ⊢ A = 𝐶    &   ⊢ B = 𝐷    ⇒   ⊢ (φ → 𝐶 ≠ 𝐷)
Theorem	3netr4g 2234	Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.)
⊢ (φ → A ≠ B)    &   ⊢ 𝐶 = A    &   ⊢ 𝐷 = B    ⇒   ⊢ (φ → 𝐶 ≠ 𝐷)
Theorem	necon3abii 2235	Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
⊢ (A = B ↔ φ)    ⇒   ⊢ (A ≠ B ↔ ¬ φ)
Theorem	necon3bbii 2236	Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (φ ↔ A = B)    ⇒   ⊢ (¬ φ ↔ A ≠ B)
Theorem	necon3bii 2237	Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
⊢ (A = B ↔ 𝐶 = 𝐷)    ⇒   ⊢ (A ≠ B ↔ 𝐶 ≠ 𝐷)
Theorem	necon3abid 2238	Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
⊢ (φ → (A = B ↔ ψ))    ⇒   ⊢ (φ → (A ≠ B ↔ ¬ ψ))
Theorem	necon3bbid 2239	Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
⊢ (φ → (ψ ↔ A = B))    ⇒   ⊢ (φ → (¬ ψ ↔ A ≠ B))
Theorem	necon3bid 2240	Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (φ → (A = B ↔ 𝐶 = 𝐷))    ⇒   ⊢ (φ → (A ≠ B ↔ 𝐶 ≠ 𝐷))
Theorem	necon3ad 2241	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ (φ → (ψ → A = B))    ⇒   ⊢ (φ → (A ≠ B → ¬ ψ))
Theorem	necon3bd 2242	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ (φ → (A = B → ψ))    ⇒   ⊢ (φ → (¬ ψ → A ≠ B))
Theorem	necon3d 2243	Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
⊢ (φ → (A = B → 𝐶 = 𝐷))    ⇒   ⊢ (φ → (𝐶 ≠ 𝐷 → A ≠ B))
Theorem	nesym 2244	Characterization of inequality in terms of reversed equality (see bicom 128). (Contributed by BJ, 7-Jul-2018.)
⊢ (A ≠ B ↔ ¬ B = A)
Theorem	nesymi 2245	Inference associated with nesym 2244. (Contributed by BJ, 7-Jul-2018.)
⊢ A ≠ B    ⇒   ⊢ ¬ B = A
Theorem	nesymir 2246	Inference associated with nesym 2244. (Contributed by BJ, 7-Jul-2018.)
⊢ ¬ A = B    ⇒   ⊢ B ≠ A
Theorem	necon3i 2247	Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.)
⊢ (A = B → 𝐶 = 𝐷)    ⇒   ⊢ (𝐶 ≠ 𝐷 → A ≠ B)
Theorem	necon3ai 2248	Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ (φ → A = B)    ⇒   ⊢ (A ≠ B → ¬ φ)
Theorem	necon3bi 2249	Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ (A = B → φ)    ⇒   ⊢ (¬ φ → A ≠ B)
Theorem	necon1aidc 2250	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
⊢ (DECID φ → (¬ φ → A = B))    ⇒   ⊢ (DECID φ → (A ≠ B → φ))
Theorem	necon1bidc 2251	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
⊢ (DECID A = B → (A ≠ B → φ))    ⇒   ⊢ (DECID A = B → (¬ φ → A = B))
Theorem	necon1idc 2252	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (A ≠ B → 𝐶 = 𝐷)    ⇒   ⊢ (DECID A = B → (𝐶 ≠ 𝐷 → A = B))
Theorem	necon2ai 2253	Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
⊢ (A = B → ¬ φ)    ⇒   ⊢ (φ → A ≠ B)
Theorem	necon2bi 2254	Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
⊢ (φ → A ≠ B)    ⇒   ⊢ (A = B → ¬ φ)
Theorem	necon2i 2255	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
⊢ (A = B → 𝐶 ≠ 𝐷)    ⇒   ⊢ (𝐶 = 𝐷 → A ≠ B)
Theorem	necon2ad 2256	Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
⊢ (φ → (A = B → ¬ ψ))    ⇒   ⊢ (φ → (ψ → A ≠ B))
Theorem	necon2bd 2257	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (φ → (ψ → A ≠ B))    ⇒   ⊢ (φ → (A = B → ¬ ψ))
Theorem	necon2d 2258	Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
⊢ (φ → (A = B → 𝐶 ≠ 𝐷))    ⇒   ⊢ (φ → (𝐶 = 𝐷 → A ≠ B))
Theorem	necon1abiidc 2259	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID φ → (¬ φ ↔ A = B))    ⇒   ⊢ (DECID φ → (A ≠ B ↔ φ))
Theorem	necon1bbiidc 2260	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID A = B → (A ≠ B ↔ φ))    ⇒   ⊢ (DECID A = B → (¬ φ ↔ A = B))
Theorem	necon1abiddc 2261	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (φ → (DECID ψ → (¬ ψ ↔ A = B)))    ⇒   ⊢ (φ → (DECID ψ → (A ≠ B ↔ ψ)))
Theorem	necon1bbiddc 2262	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (φ → (DECID A = B → (A ≠ B ↔ ψ)))    ⇒   ⊢ (φ → (DECID A = B → (¬ ψ ↔ A = B)))
Theorem	necon2abiidc 2263	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID φ → (A = B ↔ ¬ φ))    ⇒   ⊢ (DECID φ → (φ ↔ A ≠ B))
Theorem	necon2bbii 2264	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID A = B → (φ ↔ A ≠ B))    ⇒   ⊢ (DECID A = B → (A = B ↔ ¬ φ))
Theorem	necon2abiddc 2265	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (φ → (DECID ψ → (A = B ↔ ¬ ψ)))    ⇒   ⊢ (φ → (DECID ψ → (ψ ↔ A ≠ B)))
Theorem	necon2bbiddc 2266	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (φ → (DECID A = B → (ψ ↔ A ≠ B)))    ⇒   ⊢ (φ → (DECID A = B → (A = B ↔ ¬ ψ)))
Theorem	necon4aidc 2267	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID A = B → (A ≠ B → ¬ φ))    ⇒   ⊢ (DECID A = B → (φ → A = B))
Theorem	necon4idc 2268	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID A = B → (A ≠ B → 𝐶 ≠ 𝐷))    ⇒   ⊢ (DECID A = B → (𝐶 = 𝐷 → A = B))
Theorem	necon4addc 2269	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
⊢ (φ → (DECID A = B → (A ≠ B → ¬ ψ)))    ⇒   ⊢ (φ → (DECID A = B → (ψ → A = B)))
Theorem	necon4bddc 2270	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
⊢ (φ → (DECID ψ → (¬ ψ → A ≠ B)))    ⇒   ⊢ (φ → (DECID ψ → (A = B → ψ)))
Theorem	necon4ddc 2271	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
⊢ (φ → (DECID A = B → (A ≠ B → 𝐶 ≠ 𝐷)))    ⇒   ⊢ (φ → (DECID A = B → (𝐶 = 𝐷 → A = B)))
Theorem	necon4abiddc 2272	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 18-May-2018.)
⊢ (φ → (DECID A = B → (DECID ψ → (A ≠ B ↔ ¬ ψ))))    ⇒   ⊢ (φ → (DECID A = B → (DECID ψ → (A = B ↔ ψ))))
Theorem	necon4bbiddc 2273	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (φ → (DECID ψ → (DECID A = B → (¬ ψ ↔ A ≠ B))))    ⇒   ⊢ (φ → (DECID ψ → (DECID A = B → (ψ ↔ A = B))))
Theorem	necon4biddc 2274	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (φ → (DECID A = B → (DECID 𝐶 = 𝐷 → (A ≠ B ↔ 𝐶 ≠ 𝐷))))    ⇒   ⊢ (φ → (DECID A = B → (DECID 𝐶 = 𝐷 → (A = B ↔ 𝐶 = 𝐷))))
Theorem	necon1addc 2275	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (φ → (DECID ψ → (¬ ψ → A = B)))    ⇒   ⊢ (φ → (DECID ψ → (A ≠ B → ψ)))
Theorem	necon1bddc 2276	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (φ → (DECID A = B → (A ≠ B → ψ)))    ⇒   ⊢ (φ → (DECID A = B → (¬ ψ → A = B)))
Theorem	necon1ddc 2277	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (φ → (DECID A = B → (A ≠ B → 𝐶 = 𝐷)))    ⇒   ⊢ (φ → (DECID A = B → (𝐶 ≠ 𝐷 → A = B)))
Theorem	neneqad 2278	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2221. One-way deduction form of df-ne 2203. (Contributed by David Moews, 28-Feb-2017.)
⊢ (φ → ¬ A = B)    ⇒   ⊢ (φ → A ≠ B)
Theorem	nebidc 2279	Contraposition law for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (DECID A = B → (DECID 𝐶 = 𝐷 → ((A = B ↔ 𝐶 = 𝐷) ↔ (A ≠ B ↔ 𝐶 ≠ 𝐷))))
Theorem	pm13.18 2280	Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((A = B ∧ A ≠ 𝐶) → B ≠ 𝐶)
Theorem	pm13.181 2281	Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((A = B ∧ B ≠ 𝐶) → A ≠ 𝐶)
Theorem	pm2.21ddne 2282	A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
⊢ (φ → A = B)    &   ⊢ (φ → A ≠ B)    ⇒   ⊢ (φ → ψ)
Theorem	necom 2283	Commutation of inequality. (Contributed by NM, 14-May-1999.)
⊢ (A ≠ B ↔ B ≠ A)
Theorem	necomi 2284	Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
⊢ A ≠ B    ⇒   ⊢ B ≠ A
Theorem	necomd 2285	Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
⊢ (φ → A ≠ B)    ⇒   ⊢ (φ → B ≠ A)
Theorem	neanior 2286	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
⊢ ((A ≠ B ∧ 𝐶 ≠ 𝐷) ↔ ¬ (A = B ∨ 𝐶 = 𝐷))
Theorem	ne3anior 2287	A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.) (Proof rewritten by Jim Kingdon, 19-May-2018.)
⊢ ((A ≠ B ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹) ↔ ¬ (A = B ∨ 𝐶 = 𝐷 ∨ 𝐸 = 𝐹))
Theorem	nemtbir 2288	An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.)
⊢ A ≠ B    &   ⊢ (φ ↔ A = B)    ⇒   ⊢ ¬ φ
Theorem	nelne1 2289	Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.)
⊢ ((A ∈ B ∧ ¬ A ∈ 𝐶) → B ≠ 𝐶)
Theorem	nelne2 2290	Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.)
⊢ ((A ∈ 𝐶 ∧ ¬ B ∈ 𝐶) → A ≠ B)
Theorem	nfne 2291	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx A ≠ B
Theorem	nfned 2292	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ (φ → ℲxA)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → Ⅎx A ≠ B)
2.1.4.2  Negated membership
Theorem	neli 2293	Inference associated with df-nel 2204. (Contributed by BJ, 7-Jul-2018.)
⊢ A ∉ B    ⇒   ⊢ ¬ A ∈ B
Theorem	nelir 2294	Inference associated with df-nel 2204. (Contributed by BJ, 7-Jul-2018.)
⊢ ¬ A ∈ B    ⇒   ⊢ A ∉ B
Theorem	neleq1 2295	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
⊢ (A = B → (A ∉ 𝐶 ↔ B ∉ 𝐶))
Theorem	neleq2 2296	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
⊢ (A = B → (𝐶 ∉ A ↔ 𝐶 ∉ B))
Theorem	neleq12d 2297	Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.)
⊢ (φ → A = B)    &   ⊢ (φ → 𝐶 = 𝐷)    ⇒   ⊢ (φ → (A ∉ 𝐶 ↔ B ∉ 𝐷))
Theorem	nfnel 2298	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx A ∉ B
Theorem	nfneld 2299	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ (φ → ℲxA)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → Ⅎx A ∉ B)
2.1.5  Restricted quantification
Syntax	wral 2300	Extend wff notation to include restricted universal quantification.
wff ∀x ∈ A φ