P. 25 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2401-2500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	3netr3g 2401	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	3netr4g 2402	Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	necon3abii 2403	Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
⊢ (𝐴 = 𝐵 ↔ 𝜑)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑)
Theorem	necon3bbii 2404	Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (𝜑 ↔ 𝐴 = 𝐵)    ⇒   ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵)
Theorem	necon3bii 2405	Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)
Theorem	necon3abid 2406	Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))
Theorem	necon3bbid 2407	Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))
Theorem	necon3bid 2408	Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))
Theorem	necon3ad 2409	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓))
Theorem	necon3bd 2410	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))    ⇒   ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))
Theorem	necon3d 2411	Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 = 𝐷))    ⇒   ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵))
Theorem	nesym 2412	Characterization of inequality in terms of reversed equality (see bicom 140). (Contributed by BJ, 7-Jul-2018.)
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)
Theorem	nesymi 2413	Inference associated with nesym 2412. (Contributed by BJ, 7-Jul-2018.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ ¬ 𝐵 = 𝐴
Theorem	nesymir 2414	Inference associated with nesym 2412. (Contributed by BJ, 7-Jul-2018.)
⊢ ¬ 𝐴 = 𝐵    ⇒   ⊢ 𝐵 ≠ 𝐴
Theorem	necon3i 2415	Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.)
⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷)    ⇒   ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵)
Theorem	necon3ai 2416	Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑)
Theorem	necon3bi 2417	Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ (𝐴 = 𝐵 → 𝜑)    ⇒   ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵)
Theorem	necon1aidc 2418	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
⊢ (DECID 𝜑 → (¬ 𝜑 → 𝐴 = 𝐵))    ⇒   ⊢ (DECID 𝜑 → (𝐴 ≠ 𝐵 → 𝜑))
Theorem	necon1bidc 2419	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
⊢ (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑))    ⇒   ⊢ (DECID 𝐴 = 𝐵 → (¬ 𝜑 → 𝐴 = 𝐵))
Theorem	necon1idc 2420	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (𝐴 ≠ 𝐵 → 𝐶 = 𝐷)    ⇒   ⊢ (DECID 𝐴 = 𝐵 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵))
Theorem	necon2ai 2421	Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
⊢ (𝐴 = 𝐵 → ¬ 𝜑)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	necon2bi 2422	Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝐴 = 𝐵 → ¬ 𝜑)
Theorem	necon2i 2423	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
⊢ (𝐴 = 𝐵 → 𝐶 ≠ 𝐷)    ⇒   ⊢ (𝐶 = 𝐷 → 𝐴 ≠ 𝐵)
Theorem	necon2ad 2424	Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))    ⇒   ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵))
Theorem	necon2bd 2425	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
Theorem	necon2d 2426	Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 ≠ 𝐷))    ⇒   ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 ≠ 𝐵))
Theorem	necon1abiidc 2427	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID 𝜑 → (¬ 𝜑 ↔ 𝐴 = 𝐵))    ⇒   ⊢ (DECID 𝜑 → (𝐴 ≠ 𝐵 ↔ 𝜑))
Theorem	necon1bbiidc 2428	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 ↔ 𝜑))    ⇒   ⊢ (DECID 𝐴 = 𝐵 → (¬ 𝜑 ↔ 𝐴 = 𝐵))
Theorem	necon1abiddc 2429	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (𝜑 → (DECID 𝜓 → (¬ 𝜓 ↔ 𝐴 = 𝐵)))    ⇒   ⊢ (𝜑 → (DECID 𝜓 → (𝐴 ≠ 𝐵 ↔ 𝜓)))
Theorem	necon1bbiddc 2430	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 ↔ 𝜓)))    ⇒   ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (¬ 𝜓 ↔ 𝐴 = 𝐵)))
Theorem	necon2abiidc 2431	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID 𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜑))    ⇒   ⊢ (DECID 𝜑 → (𝜑 ↔ 𝐴 ≠ 𝐵))
Theorem	necon2bbiidc 2432	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID 𝐴 = 𝐵 → (𝜑 ↔ 𝐴 ≠ 𝐵))    ⇒   ⊢ (DECID 𝐴 = 𝐵 → (𝐴 = 𝐵 ↔ ¬ 𝜑))
Theorem	necon2abiddc 2433	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (𝜑 → (DECID 𝜓 → (𝐴 = 𝐵 ↔ ¬ 𝜓)))    ⇒   ⊢ (𝜑 → (DECID 𝜓 → (𝜓 ↔ 𝐴 ≠ 𝐵)))
Theorem	necon2bbiddc 2434	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝜓 ↔ 𝐴 ≠ 𝐵)))    ⇒   ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 = 𝐵 ↔ ¬ 𝜓)))
Theorem	necon4aidc 2435	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → ¬ 𝜑))    ⇒   ⊢ (DECID 𝐴 = 𝐵 → (𝜑 → 𝐴 = 𝐵))
Theorem	necon4idc 2436	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝐶 ≠ 𝐷))    ⇒   ⊢ (DECID 𝐴 = 𝐵 → (𝐶 = 𝐷 → 𝐴 = 𝐵))
Theorem	necon4addc 2437	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → ¬ 𝜓)))    ⇒   ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝜓 → 𝐴 = 𝐵)))
Theorem	necon4bddc 2438	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
⊢ (𝜑 → (DECID 𝜓 → (¬ 𝜓 → 𝐴 ≠ 𝐵)))    ⇒   ⊢ (𝜑 → (DECID 𝜓 → (𝐴 = 𝐵 → 𝜓)))
Theorem	necon4ddc 2439	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝐶 ≠ 𝐷)))    ⇒   ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐶 = 𝐷 → 𝐴 = 𝐵)))
Theorem	necon4abiddc 2440	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 18-May-2018.)
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝜓 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))))    ⇒   ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝜓 → (𝐴 = 𝐵 ↔ 𝜓))))
Theorem	necon4bbiddc 2441	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (𝜑 → (DECID 𝜓 → (DECID 𝐴 = 𝐵 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))))    ⇒   ⊢ (𝜑 → (DECID 𝜓 → (DECID 𝐴 = 𝐵 → (𝜓 ↔ 𝐴 = 𝐵))))
Theorem	necon4biddc 2442	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))))    ⇒   ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))))
Theorem	necon1addc 2443	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (𝜑 → (DECID 𝜓 → (¬ 𝜓 → 𝐴 = 𝐵)))    ⇒   ⊢ (𝜑 → (DECID 𝜓 → (𝐴 ≠ 𝐵 → 𝜓)))
Theorem	necon1bddc 2444	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜓)))    ⇒   ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (¬ 𝜓 → 𝐴 = 𝐵)))
Theorem	necon1ddc 2445	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝐶 = 𝐷)))    ⇒   ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵)))
Theorem	neneqad 2446	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2388. One-way deduction form of df-ne 2368. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → ¬ 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	nebidc 2447	Contraposition law for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → ((𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ↔ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))))
Theorem	pm13.18 2448	Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐶) → 𝐵 ≠ 𝐶)
Theorem	pm13.181 2449	Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ≠ 𝐶) → 𝐴 ≠ 𝐶)
Theorem	pm2.21ddne 2450	A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	necom 2451	Commutation of inequality. (Contributed by NM, 14-May-1999.)
⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
Theorem	necomi 2452	Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ 𝐵 ≠ 𝐴
Theorem	necomd 2453	Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐴)
Theorem	neanior 2454	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))
Theorem	ne3anior 2455	A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.) (Proof rewritten by Jim Kingdon, 19-May-2018.)
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷 ∨ 𝐸 = 𝐹))
Theorem	nemtbir 2456	An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ (𝜑 ↔ 𝐴 = 𝐵)    ⇒   ⊢ ¬ 𝜑
Theorem	nelne1 2457	Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.)
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶)
Theorem	nelne2 2458	Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵)
Theorem	nelelne 2459	Two classes are different if they don't belong to the same class. (Contributed by Rodolfo Medina, 17-Oct-2010.) (Proof shortened by AV, 10-May-2020.)
⊢ (¬ 𝐴 ∈ 𝐵 → (𝐶 ∈ 𝐵 → 𝐶 ≠ 𝐴))
Theorem	nfne 2460	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵
Theorem	nfned 2461	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 ≠ 𝐵)
2.1.4.2  Negated membership
Syntax	wnel 2462	Extend wff notation to include negated membership.
wff 𝐴 ∉ 𝐵
Definition	df-nel 2463	Define negated membership. (Contributed by NM, 7-Aug-1994.)
⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)
Theorem	neli 2464	Inference associated with df-nel 2463. (Contributed by BJ, 7-Jul-2018.)
⊢ 𝐴 ∉ 𝐵    ⇒   ⊢ ¬ 𝐴 ∈ 𝐵
Theorem	nelir 2465	Inference associated with df-nel 2463. (Contributed by BJ, 7-Jul-2018.)
⊢ ¬ 𝐴 ∈ 𝐵    ⇒   ⊢ 𝐴 ∉ 𝐵
Theorem	neleq1 2466	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶))
Theorem	neleq2 2467	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
⊢ (𝐴 = 𝐵 → (𝐶 ∉ 𝐴 ↔ 𝐶 ∉ 𝐵))
Theorem	neleq12d 2468	Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐷))
Theorem	nfnel 2469	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ∉ 𝐵
Theorem	nfneld 2470	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∉ 𝐵)
Theorem	elnelne1 2471	Two classes are different if they don't contain the same element. (Contributed by AV, 28-Jan-2020.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∉ 𝐶) → 𝐵 ≠ 𝐶)
Theorem	elnelne2 2472	Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∉ 𝐶) → 𝐴 ≠ 𝐵)
Theorem	nelcon3d 2473	Contrapositive law deduction for negated membership. (Contributed by AV, 28-Jan-2020.)
⊢ (𝜑 → (𝐴 ∈ 𝐵 → 𝐶 ∈ 𝐷))    ⇒   ⊢ (𝜑 → (𝐶 ∉ 𝐷 → 𝐴 ∉ 𝐵))
Theorem	elnelall 2474	A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
⊢ (𝐴 ∈ 𝐵 → (𝐴 ∉ 𝐵 → 𝜑))
2.1.5  Restricted quantification
Syntax	wral 2475	Extend wff notation to include restricted universal quantification.
wff ∀𝑥 ∈ 𝐴 𝜑
Syntax	wrex 2476	Extend wff notation to include restricted existential quantification.
wff ∃𝑥 ∈ 𝐴 𝜑
Syntax	wreu 2477	Extend wff notation to include restricted existential uniqueness.
wff ∃!𝑥 ∈ 𝐴 𝜑
Syntax	wrmo 2478	Extend wff notation to include restricted "at most one".
wff ∃*𝑥 ∈ 𝐴 𝜑
Syntax	crab 2479	Extend class notation to include the restricted class abstraction (class builder).
class {𝑥 ∈ 𝐴 ∣ 𝜑}
Definition	df-ral 2480	Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
Definition	df-rex 2481	Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Definition	df-reu 2482	Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Definition	df-rmo 2483	Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Definition	df-rab 2484	Define a restricted class abstraction (class builder), which is the class of all 𝑥 in 𝐴 such that 𝜑 is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
Theorem	ralnex 2485	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
Theorem	rexnalim 2486	Relationship between restricted universal and existential quantifiers. In classical logic this would be a biconditional. (Contributed by Jim Kingdon, 17-Aug-2018.)
⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 → ¬ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	nnral 2487	The double negation of a universal quantification implies the universal quantification of the double negation. Restricted quantifier version of nnal 1663. (Contributed by Jim Kingdon, 1-Aug-2024.)
⊢ (¬ ¬ ∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑)
Theorem	dfrex2dc 2488	Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 29-Jun-2022.)
⊢ (DECID ∃𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑))
Theorem	ralexim 2489	Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑)
Theorem	rexalim 2490	Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
Theorem	ralbida 2491	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Oct-2003.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexbida 2492	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 6-Oct-2003.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	ralbidva 2493*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexbidva 2494*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	ralbid 2495	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 27-Jun-1998.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexbid 2496	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 27-Jun-1998.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	ralbidv 2497*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexbidv 2498*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	ralbidv2 2499*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Apr-1997.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	rexbidv2 2500*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 22-May-1999.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))