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	nelelne 2401	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 2402	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵
Theorem	nfned 2403	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 2404	Extend wff notation to include negated membership.
wff 𝐴 ∉ 𝐵
Definition	df-nel 2405	Define negated membership. (Contributed by NM, 7-Aug-1994.)
⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)
Theorem	neli 2406	Inference associated with df-nel 2405. (Contributed by BJ, 7-Jul-2018.)
⊢ 𝐴 ∉ 𝐵    ⇒   ⊢ ¬ 𝐴 ∈ 𝐵
Theorem	nelir 2407	Inference associated with df-nel 2405. (Contributed by BJ, 7-Jul-2018.)
⊢ ¬ 𝐴 ∈ 𝐵    ⇒   ⊢ 𝐴 ∉ 𝐵
Theorem	neleq1 2408	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶))
Theorem	neleq2 2409	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
⊢ (𝐴 = 𝐵 → (𝐶 ∉ 𝐴 ↔ 𝐶 ∉ 𝐵))
Theorem	neleq12d 2410	Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐷))
Theorem	nfnel 2411	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ∉ 𝐵
Theorem	nfneld 2412	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∉ 𝐵)
Theorem	elnelne1 2413	Two classes are different if they don't contain the same element. (Contributed by AV, 28-Jan-2020.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∉ 𝐶) → 𝐵 ≠ 𝐶)
Theorem	elnelne2 2414	Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∉ 𝐶) → 𝐴 ≠ 𝐵)
Theorem	nelcon3d 2415	Contrapositive law deduction for negated membership. (Contributed by AV, 28-Jan-2020.)
⊢ (𝜑 → (𝐴 ∈ 𝐵 → 𝐶 ∈ 𝐷))    ⇒   ⊢ (𝜑 → (𝐶 ∉ 𝐷 → 𝐴 ∉ 𝐵))
Theorem	elnelall 2416	A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
⊢ (𝐴 ∈ 𝐵 → (𝐴 ∉ 𝐵 → 𝜑))
2.1.5  Restricted quantification
Syntax	wral 2417	Extend wff notation to include restricted universal quantification.
wff ∀𝑥 ∈ 𝐴 𝜑
Syntax	wrex 2418	Extend wff notation to include restricted existential quantification.
wff ∃𝑥 ∈ 𝐴 𝜑
Syntax	wreu 2419	Extend wff notation to include restricted existential uniqueness.
wff ∃!𝑥 ∈ 𝐴 𝜑
Syntax	wrmo 2420	Extend wff notation to include restricted "at most one."
wff ∃*𝑥 ∈ 𝐴 𝜑
Syntax	crab 2421	Extend class notation to include the restricted class abstraction (class builder).
class {𝑥 ∈ 𝐴 ∣ 𝜑}
Definition	df-ral 2422	Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
Definition	df-rex 2423	Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Definition	df-reu 2424	Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Definition	df-rmo 2425	Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Definition	df-rab 2426	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 2427	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
Theorem	rexnalim 2428	Relationship between restricted universal and existential quantifiers. In classical logic this would be a biconditional. (Contributed by Jim Kingdon, 17-Aug-2018.)
⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 → ¬ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	dfrex2dc 2429	Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 29-Jun-2022.)
⊢ (DECID ∃𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑))
Theorem	ralexim 2430	Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑)
Theorem	rexalim 2431	Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
Theorem	ralbida 2432	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Oct-2003.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexbida 2433	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 6-Oct-2003.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	ralbidva 2434*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexbidva 2435*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	ralbid 2436	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 27-Jun-1998.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexbid 2437	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 27-Jun-1998.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	ralbidv 2438*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexbidv 2439*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	ralbidv2 2440*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Apr-1997.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	rexbidv2 2441*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 22-May-1999.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	ralbid2 2442	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	rexbid2 2443	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	ralbii 2444	Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)
Theorem	rexbii 2445	Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)
Theorem	2ralbii 2446	Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)
Theorem	2rexbii 2447	Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)
Theorem	ralbii2 2448	Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.)
⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐵 → 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)
Theorem	rexbii2 2449	Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)
Theorem	raleqbii 2450	Equality deduction for restricted universal quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)
Theorem	rexeqbii 2451	Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)
Theorem	ralbiia 2452	Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)
Theorem	rexbiia 2453	Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)
Theorem	2rexbiia 2454*	Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)
Theorem	r2alf 2455*	Double restricted universal quantification. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))
Theorem	r2exf 2456*	Double restricted existential quantification. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))
Theorem	r2al 2457*	Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))
Theorem	r2ex 2458*	Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))
Theorem	2ralbida 2459*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 24-Feb-2004.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))
Theorem	2ralbidva 2460*	Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 4-Mar-1997.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))
Theorem	2rexbidva 2461*	Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 15-Dec-2004.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))
Theorem	2ralbidv 2462*	Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))
Theorem	2rexbidv 2463*	Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))
Theorem	rexralbidv 2464*	Formula-building rule for restricted quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))
Theorem	ralinexa 2465	A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
Theorem	risset 2466*	Two ways to say "𝐴 belongs to 𝐵." (Contributed by NM, 22-Nov-1994.)
⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴)
Theorem	hbral 2467	Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by David Abernethy, 13-Dec-2009.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∀𝑦 ∈ 𝐴 𝜑 → ∀𝑥∀𝑦 ∈ 𝐴 𝜑)
Theorem	hbra1 2468	𝑥 is not free in ∀𝑥 ∈ 𝐴𝜑. (Contributed by NM, 18-Oct-1996.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥∀𝑥 ∈ 𝐴 𝜑)
Theorem	nfra1 2469	𝑥 is not free in ∀𝑥 ∈ 𝐴𝜑. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑
Theorem	nfraldxy 2470*	Not-free for restricted universal quantification where 𝑥 and 𝑦 are distinct. See nfraldya 2472 for a version with 𝑦 and 𝐴 distinct instead. (Contributed by Jim Kingdon, 29-May-2018.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜓)
Theorem	nfrexdxy 2471*	Not-free for restricted existential quantification where 𝑥 and 𝑦 are distinct. See nfrexdya 2473 for a version with 𝑦 and 𝐴 distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜓)
Theorem	nfraldya 2472*	Not-free for restricted universal quantification where 𝑦 and 𝐴 are distinct. See nfraldxy 2470 for a version with 𝑥 and 𝑦 distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜓)
Theorem	nfrexdya 2473*	Not-free for restricted existential quantification where 𝑦 and 𝐴 are distinct. See nfrexdxy 2471 for a version with 𝑥 and 𝑦 distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜓)
Theorem	nfralxy 2474*	Not-free for restricted universal quantification where 𝑥 and 𝑦 are distinct. See nfralya 2476 for a version with 𝑦 and 𝐴 distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑
Theorem	nfrexxy 2475*	Not-free for restricted existential quantification where 𝑥 and 𝑦 are distinct. See nfrexya 2477 for a version with 𝑦 and 𝐴 distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑
Theorem	nfralya 2476*	Not-free for restricted universal quantification where 𝑦 and 𝐴 are distinct. See nfralxy 2474 for a version with 𝑥 and 𝑦 distinct instead. (Contributed by Jim Kingdon, 3-Jun-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑
Theorem	nfrexya 2477*	Not-free for restricted existential quantification where 𝑦 and 𝐴 are distinct. See nfrexxy 2475 for a version with 𝑥 and 𝑦 distinct instead. (Contributed by Jim Kingdon, 3-Jun-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑
Theorem	nfra2xy 2478*	Not-free given two restricted quantifiers. (Contributed by Jim Kingdon, 20-Aug-2018.)
⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑
Theorem	nfre1 2479	𝑥 is not free in ∃𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑
Theorem	r3al 2480*	Triple restricted universal quantification. (Contributed by NM, 19-Nov-1995.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑))
Theorem	alral 2481	Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.)
⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexex 2482	Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥𝜑)
Theorem	rsp 2483	Restricted specialization. (Contributed by NM, 17-Oct-1996.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑))
Theorem	rspe 2484	Restricted specialization. (Contributed by NM, 12-Oct-1999.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)
Theorem	rsp2 2485	Restricted specialization. (Contributed by NM, 11-Feb-1997.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))
Theorem	rsp2e 2486	Restricted specialization. (Contributed by FL, 4-Jun-2012.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
Theorem	rspec 2487	Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
⊢ ∀𝑥 ∈ 𝐴 𝜑    ⇒   ⊢ (𝑥 ∈ 𝐴 → 𝜑)
Theorem	rgen 2488	Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
⊢ (𝑥 ∈ 𝐴 → 𝜑)    ⇒   ⊢ ∀𝑥 ∈ 𝐴 𝜑
Theorem	rgen2a 2489*	Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 are not required to be disjoint. This proof illustrates the use of dvelim 1993. Usage of rgen2 2521 instead is highly encouraged. (Contributed by NM, 23-Nov-1994.) (Proof rewritten by Jim Kingdon, 1-Jun-2018.) (New usage is discouraged.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝜑)    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑
Theorem	rgenw 2490	Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
⊢ 𝜑    ⇒   ⊢ ∀𝑥 ∈ 𝐴 𝜑
Theorem	rgen2w 2491	Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 needn't be distinct. (Contributed by NM, 18-Jun-2014.)
⊢ 𝜑    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑
Theorem	mprg 2492	Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → 𝜓)    &   ⊢ (𝑥 ∈ 𝐴 → 𝜑)    ⇒   ⊢ 𝜓
Theorem	mprgbir 2493	Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝑥 ∈ 𝐴 → 𝜓)    ⇒   ⊢ 𝜑
Theorem	ralim 2494	Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
Theorem	ralimi2 2495	Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.)
⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐵 → 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓)
Theorem	ralimia 2496	Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	ralimiaa 2497	Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	ralimi 2498	Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	2ralimi 2499	Inference quantifying both antecedent and consequent two times, with strong hypothesis. (Contributed by AV, 3-Dec-2021.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)
Theorem	ral2imi 2500	Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))