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	rexbidva 2301*	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 9-Mar-1997.)
⊢ ((φ ∧ x ∈ A) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))
Theorem	ralbid 2302	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.)
⊢ Ⅎxφ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ))
Theorem	rexbid 2303	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.)
⊢ Ⅎxφ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))
Theorem	ralbidv 2304*	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ))
Theorem	rexbidv 2305*	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))
Theorem	ralbidv2 2306*	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Apr-1997.)
⊢ (φ → ((x ∈ A → ψ) ↔ (x ∈ B → χ)))    ⇒   ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ B χ))
Theorem	rexbidv2 2307*	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 22-May-1999.)
⊢ (φ → ((x ∈ A ∧ ψ) ↔ (x ∈ B ∧ χ)))    ⇒   ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ B χ))
Theorem	ralbii 2308	Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (∀x ∈ A φ ↔ ∀x ∈ A ψ)
Theorem	rexbii 2309	Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (∃x ∈ A φ ↔ ∃x ∈ A ψ)
Theorem	2ralbii 2310	Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (∀x ∈ A ∀y ∈ B φ ↔ ∀x ∈ A ∀y ∈ B ψ)
Theorem	2rexbii 2311	Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (∃x ∈ A ∃y ∈ B φ ↔ ∃x ∈ A ∃y ∈ B ψ)
Theorem	ralbii2 2312	Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.)
⊢ ((x ∈ A → φ) ↔ (x ∈ B → ψ))    ⇒   ⊢ (∀x ∈ A φ ↔ ∀x ∈ B ψ)
Theorem	rexbii2 2313	Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.)
⊢ ((x ∈ A ∧ φ) ↔ (x ∈ B ∧ ψ))    ⇒   ⊢ (∃x ∈ A φ ↔ ∃x ∈ B ψ)
Theorem	raleqbii 2314	Equality deduction for restricted universal quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
⊢ A = B    &   ⊢ (ψ ↔ χ)    ⇒   ⊢ (∀x ∈ A ψ ↔ ∀x ∈ B χ)
Theorem	rexeqbii 2315	Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
⊢ A = B    &   ⊢ (ψ ↔ χ)    ⇒   ⊢ (∃x ∈ A ψ ↔ ∃x ∈ B χ)
Theorem	ralbiia 2316	Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.)
⊢ (x ∈ A → (φ ↔ ψ))    ⇒   ⊢ (∀x ∈ A φ ↔ ∀x ∈ A ψ)
Theorem	rexbiia 2317	Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.)
⊢ (x ∈ A → (φ ↔ ψ))    ⇒   ⊢ (∃x ∈ A φ ↔ ∃x ∈ A ψ)
Theorem	2rexbiia 2318*	Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
⊢ ((x ∈ A ∧ y ∈ B) → (φ ↔ ψ))    ⇒   ⊢ (∃x ∈ A ∃y ∈ B φ ↔ ∃x ∈ A ∃y ∈ B ψ)
Theorem	r2alf 2319*	Double restricted universal quantification. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ ℲyA    ⇒   ⊢ (∀x ∈ A ∀y ∈ B φ ↔ ∀x∀y((x ∈ A ∧ y ∈ B) → φ))
Theorem	r2exf 2320*	Double restricted existential quantification. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ ℲyA    ⇒   ⊢ (∃x ∈ A ∃y ∈ B φ ↔ ∃x∃y((x ∈ A ∧ y ∈ B) ∧ φ))
Theorem	r2al 2321*	Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.)
⊢ (∀x ∈ A ∀y ∈ B φ ↔ ∀x∀y((x ∈ A ∧ y ∈ B) → φ))
Theorem	r2ex 2322*	Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.)
⊢ (∃x ∈ A ∃y ∈ B φ ↔ ∃x∃y((x ∈ A ∧ y ∈ B) ∧ φ))
Theorem	2ralbida 2323*	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 24-Feb-2004.)
⊢ Ⅎxφ    &   ⊢ Ⅎyφ    &   ⊢ ((φ ∧ (x ∈ A ∧ y ∈ B)) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ∀y ∈ B ψ ↔ ∀x ∈ A ∀y ∈ B χ))
Theorem	2ralbidva 2324*	Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.)
⊢ ((φ ∧ (x ∈ A ∧ y ∈ B)) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ∀y ∈ B ψ ↔ ∀x ∈ A ∀y ∈ B χ))
Theorem	2rexbidva 2325*	Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 15-Dec-2004.)
⊢ ((φ ∧ (x ∈ A ∧ y ∈ B)) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ∃y ∈ B ψ ↔ ∃x ∈ A ∃y ∈ B χ))
Theorem	2ralbidv 2326*	Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ∀y ∈ B ψ ↔ ∀x ∈ A ∀y ∈ B χ))
Theorem	2rexbidv 2327*	Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ∃y ∈ B ψ ↔ ∃x ∈ A ∃y ∈ B χ))
Theorem	rexralbidv 2328*	Formula-building rule for restricted quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ∀y ∈ B ψ ↔ ∃x ∈ A ∀y ∈ B χ))
Theorem	ralinexa 2329	A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.)
⊢ (∀x ∈ A (φ → ¬ ψ) ↔ ¬ ∃x ∈ A (φ ∧ ψ))
Theorem	risset 2330*	Two ways to say "A belongs to B." (Contributed by NM, 22-Nov-1994.)
⊢ (A ∈ B ↔ ∃x ∈ B x = A)
Theorem	hbral 2331	Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by David Abernethy, 13-Dec-2009.)
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (φ → ∀xφ)    ⇒   ⊢ (∀y ∈ A φ → ∀x∀y ∈ A φ)
Theorem	hbra1 2332	x is not free in ∀x ∈ Aφ. (Contributed by NM, 18-Oct-1996.)
⊢ (∀x ∈ A φ → ∀x∀x ∈ A φ)
Theorem	nfra1 2333	x is not free in ∀x ∈ Aφ. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎx∀x ∈ A φ
Theorem	nfraldxy 2334*	Not-free for restricted universal quantification where x and y are distinct. See nfraldya 2336 for a version with y and A distinct instead. (Contributed by Jim Kingdon, 29-May-2018.)
⊢ Ⅎyφ    &   ⊢ (φ → ℲxA)    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ (φ → Ⅎx∀y ∈ A ψ)
Theorem	nfrexdxy 2335*	Not-free for restricted existential quantification where x and y are distinct. See nfrexdya 2337 for a version with y and A distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
⊢ Ⅎyφ    &   ⊢ (φ → ℲxA)    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ (φ → Ⅎx∃y ∈ A ψ)
Theorem	nfraldya 2336*	Not-free for restricted universal quantification where y and A are distinct. See nfraldxy 2334 for a version with x and y distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
⊢ Ⅎyφ    &   ⊢ (φ → ℲxA)    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ (φ → Ⅎx∀y ∈ A ψ)
Theorem	nfrexdya 2337*	Not-free for restricted existential quantification where y and A are distinct. See nfrexdxy 2335 for a version with x and y distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
⊢ Ⅎyφ    &   ⊢ (φ → ℲxA)    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ (φ → Ⅎx∃y ∈ A ψ)
Theorem	nfralxy 2338*	Not-free for restricted universal quantification where x and y are distinct. See nfralya 2340 for a version with y and A distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
⊢ ℲxA    &   ⊢ Ⅎxφ    ⇒   ⊢ Ⅎx∀y ∈ A φ
Theorem	nfrexxy 2339*	Not-free for restricted existential quantification where x and y are distinct. See nfrexya 2341 for a version with y and A distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
⊢ ℲxA    &   ⊢ Ⅎxφ    ⇒   ⊢ Ⅎx∃y ∈ A φ
Theorem	nfralya 2340*	Not-free for restricted universal quantification where y and A are distinct. See nfralxy 2338 for a version with x and y distinct instead. (Contributed by Jim Kingdon, 3-Jun-2018.)
⊢ ℲxA    &   ⊢ Ⅎxφ    ⇒   ⊢ Ⅎx∀y ∈ A φ
Theorem	nfrexya 2341*	Not-free for restricted existential quantification where y and A are distinct. See nfrexxy 2339 for a version with x and y distinct instead. (Contributed by Jim Kingdon, 3-Jun-2018.)
⊢ ℲxA    &   ⊢ Ⅎxφ    ⇒   ⊢ Ⅎx∃y ∈ A φ
Theorem	nfra2xy 2342*	Not-free given two restricted quantifiers. (Contributed by Jim Kingdon, 20-Aug-2018.)
⊢ Ⅎy∀x ∈ A ∀y ∈ B φ
Theorem	nfre1 2343	x is not free in ∃x ∈ Aφ. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎx∃x ∈ A φ
Theorem	r3al 2344*	Triple restricted universal quantification. (Contributed by NM, 19-Nov-1995.)
⊢ (∀x ∈ A ∀y ∈ B ∀z ∈ 𝐶 φ ↔ ∀x∀y∀z((x ∈ A ∧ y ∈ B ∧ z ∈ 𝐶) → φ))
Theorem	alral 2345	Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.)
⊢ (∀xφ → ∀x ∈ A φ)
Theorem	rexex 2346	Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)
⊢ (∃x ∈ A φ → ∃xφ)
Theorem	rsp 2347	Restricted specialization. (Contributed by NM, 17-Oct-1996.)
⊢ (∀x ∈ A φ → (x ∈ A → φ))
Theorem	rspe 2348	Restricted specialization. (Contributed by NM, 12-Oct-1999.)
⊢ ((x ∈ A ∧ φ) → ∃x ∈ A φ)
Theorem	rsp2 2349	Restricted specialization. (Contributed by NM, 11-Feb-1997.)
⊢ (∀x ∈ A ∀y ∈ B φ → ((x ∈ A ∧ y ∈ B) → φ))
Theorem	rsp2e 2350	Restricted specialization. (Contributed by FL, 4-Jun-2012.)
⊢ ((x ∈ A ∧ y ∈ B ∧ φ) → ∃x ∈ A ∃y ∈ B φ)
Theorem	rspec 2351	Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
⊢ ∀x ∈ A φ    ⇒   ⊢ (x ∈ A → φ)
Theorem	rgen 2352	Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
⊢ (x ∈ A → φ)    ⇒   ⊢ ∀x ∈ A φ
Theorem	rgen2a 2353*	Generalization rule for restricted quantification. Note that x and y needn't be distinct (and illustrates the use of dvelimor 1876). (Contributed by NM, 23-Nov-1994.) (Proof rewritten by Jim Kingdon, 1-Jun-2018.)
⊢ ((x ∈ A ∧ y ∈ A) → φ)    ⇒   ⊢ ∀x ∈ A ∀y ∈ A φ
Theorem	rgenw 2354	Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
⊢ φ    ⇒   ⊢ ∀x ∈ A φ
Theorem	rgen2w 2355	Generalization rule for restricted quantification. Note that x and y needn't be distinct. (Contributed by NM, 18-Jun-2014.)
⊢ φ    ⇒   ⊢ ∀x ∈ A ∀y ∈ B φ
Theorem	mprg 2356	Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.)
⊢ (∀x ∈ A φ → ψ)    &   ⊢ (x ∈ A → φ)    ⇒   ⊢ ψ
Theorem	mprgbir 2357	Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)
⊢ (φ ↔ ∀x ∈ A ψ)    &   ⊢ (x ∈ A → ψ)    ⇒   ⊢ φ
Theorem	ralim 2358	Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.)
⊢ (∀x ∈ A (φ → ψ) → (∀x ∈ A φ → ∀x ∈ A ψ))
Theorem	ralimi2 2359	Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.)
⊢ ((x ∈ A → φ) → (x ∈ B → ψ))    ⇒   ⊢ (∀x ∈ A φ → ∀x ∈ B ψ)
Theorem	ralimia 2360	Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)
⊢ (x ∈ A → (φ → ψ))    ⇒   ⊢ (∀x ∈ A φ → ∀x ∈ A ψ)
Theorem	ralimiaa 2361	Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.)
⊢ ((x ∈ A ∧ φ) → ψ)    ⇒   ⊢ (∀x ∈ A φ → ∀x ∈ A ψ)
Theorem	ralimi 2362	Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
⊢ (φ → ψ)    ⇒   ⊢ (∀x ∈ A φ → ∀x ∈ A ψ)
Theorem	ral2imi 2363	Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (∀x ∈ A φ → (∀x ∈ A ψ → ∀x ∈ A χ))
Theorem	ralimdaa 2364	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-Sep-2003.)
⊢ Ⅎxφ    &   ⊢ ((φ ∧ x ∈ A) → (ψ → χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ → ∀x ∈ A χ))
Theorem	ralimdva 2365*	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
⊢ ((φ ∧ x ∈ A) → (ψ → χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ → ∀x ∈ A χ))
Theorem	ralimdv 2366*	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 8-Oct-2003.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ → ∀x ∈ A χ))
Theorem	ralimdv2 2367*	Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.)
⊢ (φ → ((x ∈ A → ψ) → (x ∈ B → χ)))    ⇒   ⊢ (φ → (∀x ∈ A ψ → ∀x ∈ B χ))
Theorem	ralrimi 2368	Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.)
⊢ Ⅎxφ    &   ⊢ (φ → (x ∈ A → ψ))    ⇒   ⊢ (φ → ∀x ∈ A ψ)
Theorem	ralrimiv 2369*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.)
⊢ (φ → (x ∈ A → ψ))    ⇒   ⊢ (φ → ∀x ∈ A ψ)
Theorem	ralrimiva 2370*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)
⊢ ((φ ∧ x ∈ A) → ψ)    ⇒   ⊢ (φ → ∀x ∈ A ψ)
Theorem	ralrimivw 2371*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
⊢ (φ → ψ)    ⇒   ⊢ (φ → ∀x ∈ A ψ)
Theorem	r19.21t 2372	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers (closed theorem version). (Contributed by NM, 1-Mar-2008.)
⊢ (Ⅎxφ → (∀x ∈ A (φ → ψ) ↔ (φ → ∀x ∈ A ψ)))
Theorem	r19.21 2373	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers. (Contributed by Scott Fenton, 30-Mar-2011.)
⊢ Ⅎxφ    ⇒   ⊢ (∀x ∈ A (φ → ψ) ↔ (φ → ∀x ∈ A ψ))
Theorem	r19.21v 2374*	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ (∀x ∈ A (φ → ψ) ↔ (φ → ∀x ∈ A ψ))
Theorem	ralrimd 2375	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 16-Feb-2004.)
⊢ Ⅎxφ    &   ⊢ Ⅎxψ    &   ⊢ (φ → (ψ → (x ∈ A → χ)))    ⇒   ⊢ (φ → (ψ → ∀x ∈ A χ))
Theorem	ralrimdv 2376*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 27-May-1998.)
⊢ (φ → (ψ → (x ∈ A → χ)))    ⇒   ⊢ (φ → (ψ → ∀x ∈ A χ))
Theorem	ralrimdva 2377*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.)
⊢ ((φ ∧ x ∈ A) → (ψ → χ))    ⇒   ⊢ (φ → (ψ → ∀x ∈ A χ))
Theorem	ralrimivv 2378*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.)
⊢ (φ → ((x ∈ A ∧ y ∈ B) → ψ))    ⇒   ⊢ (φ → ∀x ∈ A ∀y ∈ B ψ)
Theorem	ralrimivva 2379*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((φ ∧ (x ∈ A ∧ y ∈ B)) → ψ)    ⇒   ⊢ (φ → ∀x ∈ A ∀y ∈ B ψ)
Theorem	ralrimivvva 2380*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with triple quantification.) (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ ((φ ∧ (x ∈ A ∧ y ∈ B ∧ z ∈ 𝐶)) → ψ)    ⇒   ⊢ (φ → ∀x ∈ A ∀y ∈ B ∀z ∈ 𝐶 ψ)
Theorem	ralrimdvv 2381*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 1-Jun-2005.)
⊢ (φ → (ψ → ((x ∈ A ∧ y ∈ B) → χ)))    ⇒   ⊢ (φ → (ψ → ∀x ∈ A ∀y ∈ B χ))
Theorem	ralrimdvva 2382*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 2-Feb-2008.)
⊢ ((φ ∧ (x ∈ A ∧ y ∈ B)) → (ψ → χ))    ⇒   ⊢ (φ → (ψ → ∀x ∈ A ∀y ∈ B χ))
Theorem	rgen2 2383*	Generalization rule for restricted quantification. (Contributed by NM, 30-May-1999.)
⊢ ((x ∈ A ∧ y ∈ B) → φ)    ⇒   ⊢ ∀x ∈ A ∀y ∈ B φ
Theorem	rgen3 2384*	Generalization rule for restricted quantification. (Contributed by NM, 12-Jan-2008.)
⊢ ((x ∈ A ∧ y ∈ B ∧ z ∈ 𝐶) → φ)    ⇒   ⊢ ∀x ∈ A ∀y ∈ B ∀z ∈ 𝐶 φ
Theorem	r19.21bi 2385	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)
⊢ (φ → ∀x ∈ A ψ)    ⇒   ⊢ ((φ ∧ x ∈ A) → ψ)
Theorem	rspec2 2386	Specialization rule for restricted quantification. (Contributed by NM, 20-Nov-1994.)
⊢ ∀x ∈ A ∀y ∈ B φ    ⇒   ⊢ ((x ∈ A ∧ y ∈ B) → φ)
Theorem	rspec3 2387	Specialization rule for restricted quantification. (Contributed by NM, 20-Nov-1994.)
⊢ ∀x ∈ A ∀y ∈ B ∀z ∈ 𝐶 φ    ⇒   ⊢ ((x ∈ A ∧ y ∈ B ∧ z ∈ 𝐶) → φ)
Theorem	r19.21be 2388	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 21-Nov-1994.)
⊢ (φ → ∀x ∈ A ψ)    ⇒   ⊢ ∀x ∈ A (φ → ψ)
Theorem	nrex 2389	Inference adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.)
⊢ (x ∈ A → ¬ ψ)    ⇒   ⊢ ¬ ∃x ∈ A ψ
Theorem	nrexdv 2390*	Deduction adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.)
⊢ ((φ ∧ x ∈ A) → ¬ ψ)    ⇒   ⊢ (φ → ¬ ∃x ∈ A ψ)
Theorem	rexim 2391	Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ (∀x ∈ A (φ → ψ) → (∃x ∈ A φ → ∃x ∈ A ψ))
Theorem	reximia 2392	Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.)
⊢ (x ∈ A → (φ → ψ))    ⇒   ⊢ (∃x ∈ A φ → ∃x ∈ A ψ)
Theorem	reximi2 2393	Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 8-Nov-2004.)
⊢ ((x ∈ A ∧ φ) → (x ∈ B ∧ ψ))    ⇒   ⊢ (∃x ∈ A φ → ∃x ∈ B ψ)
Theorem	reximi 2394	Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)
⊢ (φ → ψ)    ⇒   ⊢ (∃x ∈ A φ → ∃x ∈ A ψ)
Theorem	reximdai 2395	Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.)
⊢ Ⅎxφ    &   ⊢ (φ → (x ∈ A → (ψ → χ)))    ⇒   ⊢ (φ → (∃x ∈ A ψ → ∃x ∈ A χ))
Theorem	reximdv2 2396*	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.)
⊢ (φ → ((x ∈ A ∧ ψ) → (x ∈ B ∧ χ)))    ⇒   ⊢ (φ → (∃x ∈ A ψ → ∃x ∈ B χ))
Theorem	reximdvai 2397*	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 14-Nov-2002.)
⊢ (φ → (x ∈ A → (ψ → χ)))    ⇒   ⊢ (φ → (∃x ∈ A ψ → ∃x ∈ A χ))
Theorem	reximdv 2398*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∃x ∈ A ψ → ∃x ∈ A χ))
Theorem	reximdva 2399*	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
⊢ ((φ ∧ x ∈ A) → (ψ → χ))    ⇒   ⊢ (φ → (∃x ∈ A ψ → ∃x ∈ A χ))
Theorem	r19.12 2400*	Theorem 19.12 of [Margaris] p. 89 with restricted quantifiers. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ (∃x ∈ A ∀y ∈ B φ → ∀y ∈ B ∃x ∈ A φ)