P. 26 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2501-2600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nfraldya 2501*	Not-free for restricted universal quantification where 𝑦 and 𝐴 are distinct. See nfraldxy 2499 for a version with 𝑥 and 𝑦 distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜓)
Theorem	nfrexdya 2502*	Not-free for restricted existential quantification where 𝑦 and 𝐴 are distinct. See nfrexdxy 2500 for a version with 𝑥 and 𝑦 distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜓)
Theorem	nfralw 2503*	Bound-variable hypothesis builder for restricted quantification. See nfralya 2506 for a version with 𝑦 and 𝐴 distinct instead of 𝑥 and 𝑦. (Contributed by NM, 1-Sep-1999.) (Revised by Gino Giotto, 10-Jan-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑
Theorem	nfralxy 2504*	Old name for nfralw 2503. (Contributed by Jim Kingdon, 30-May-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑
Theorem	nfrexxy 2505*	Not-free for restricted existential quantification where 𝑥 and 𝑦 are distinct. See nfrexya 2507 for a version with 𝑦 and 𝐴 distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑
Theorem	nfralya 2506*	Not-free for restricted universal quantification where 𝑦 and 𝐴 are distinct. See nfralxy 2504 for a version with 𝑥 and 𝑦 distinct instead. (Contributed by Jim Kingdon, 3-Jun-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑
Theorem	nfrexya 2507*	Not-free for restricted existential quantification where 𝑦 and 𝐴 are distinct. See nfrexxy 2505 for a version with 𝑥 and 𝑦 distinct instead. (Contributed by Jim Kingdon, 3-Jun-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑
Theorem	nfra2xy 2508*	Not-free given two restricted quantifiers. (Contributed by Jim Kingdon, 20-Aug-2018.)
⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑
Theorem	nfre1 2509	𝑥 is not free in ∃𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑
Theorem	r3al 2510*	Triple restricted universal quantification. (Contributed by NM, 19-Nov-1995.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑))
Theorem	alral 2511	Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.)
⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexex 2512	Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥𝜑)
Theorem	rsp 2513	Restricted specialization. (Contributed by NM, 17-Oct-1996.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑))
Theorem	rspa 2514	Restricted specialization. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜑)
Theorem	rspe 2515	Restricted specialization. (Contributed by NM, 12-Oct-1999.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)
Theorem	rsp2 2516	Restricted specialization. (Contributed by NM, 11-Feb-1997.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))
Theorem	rsp2e 2517	Restricted specialization. (Contributed by FL, 4-Jun-2012.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
Theorem	rspec 2518	Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
⊢ ∀𝑥 ∈ 𝐴 𝜑    ⇒   ⊢ (𝑥 ∈ 𝐴 → 𝜑)
Theorem	rgen 2519	Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
⊢ (𝑥 ∈ 𝐴 → 𝜑)    ⇒   ⊢ ∀𝑥 ∈ 𝐴 𝜑
Theorem	rgen2a 2520*	Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 are not required to be disjoint. This proof illustrates the use of dvelim 2005. Usage of rgen2 2552 instead is highly encouraged. (Contributed by NM, 23-Nov-1994.) (Proof rewritten by Jim Kingdon, 1-Jun-2018.) (New usage is discouraged.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝜑)    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑
Theorem	rgenw 2521	Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
⊢ 𝜑    ⇒   ⊢ ∀𝑥 ∈ 𝐴 𝜑
Theorem	rgen2w 2522	Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 needn't be distinct. (Contributed by NM, 18-Jun-2014.)
⊢ 𝜑    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑
Theorem	mprg 2523	Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → 𝜓)    &   ⊢ (𝑥 ∈ 𝐴 → 𝜑)    ⇒   ⊢ 𝜓
Theorem	mprgbir 2524	Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝑥 ∈ 𝐴 → 𝜓)    ⇒   ⊢ 𝜑
Theorem	ralim 2525	Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
Theorem	ralimi2 2526	Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.)
⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐵 → 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓)
Theorem	ralimia 2527	Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	ralimiaa 2528	Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	ralimi 2529	Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	2ralimi 2530	Inference quantifying both antecedent and consequent two times, with strong hypothesis. (Contributed by AV, 3-Dec-2021.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)
Theorem	ral2imi 2531	Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
Theorem	ralimdaa 2532	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-Sep-2003.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
Theorem	ralimdva 2533*	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
Theorem	ralimdv 2534*	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 8-Oct-2003.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
Theorem	ralimdvva 2535*	Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1445). (Contributed by AV, 27-Nov-2019.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))
Theorem	ralimdv2 2536*	Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐵 → 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒))
Theorem	ralrimi 2537	Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	ralrimiv 2538*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	ralrimiva 2539*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	ralrimivw 2540*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	r19.21t 2541	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers (closed theorem version). (Contributed by NM, 1-Mar-2008.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)))
Theorem	r19.21 2542	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers. (Contributed by Scott Fenton, 30-Mar-2011.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
Theorem	r19.21v 2543*	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
Theorem	ralrimd 2544	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 16-Feb-2004.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒)))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
Theorem	ralrimdv 2545*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 27-May-1998.)
⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒)))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
Theorem	ralrimdva 2546*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
Theorem	ralrimivv 2547*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)
Theorem	ralrimivva 2548*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)
Theorem	ralrimivvva 2549*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with triple quantification.) (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓)
Theorem	ralrimdvv 2550*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 1-Jun-2005.)
⊢ (𝜑 → (𝜓 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜒)))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))
Theorem	ralrimdvva 2551*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 2-Feb-2008.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))
Theorem	rgen2 2552*	Generalization rule for restricted quantification. (Contributed by NM, 30-May-1999.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑
Theorem	rgen3 2553*	Generalization rule for restricted quantification. (Contributed by NM, 12-Jan-2008.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑)    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑
Theorem	r19.21bi 2554	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)
Theorem	rspec2 2555	Specialization rule for restricted quantification. (Contributed by NM, 20-Nov-1994.)
⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑    ⇒   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)
Theorem	rspec3 2556	Specialization rule for restricted quantification. (Contributed by NM, 20-Nov-1994.)
⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑    ⇒   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑)
Theorem	r19.21be 2557	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 21-Nov-1994.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)
Theorem	nrex 2558	Inference adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.)
⊢ (𝑥 ∈ 𝐴 → ¬ 𝜓)    ⇒   ⊢ ¬ ∃𝑥 ∈ 𝐴 𝜓
Theorem	nrexdv 2559*	Deduction adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ ∃𝑥 ∈ 𝐴 𝜓)
Theorem	rexim 2560	Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
Theorem	reximia 2561	Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	reximi2 2562	Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 8-Nov-2004.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
Theorem	reximi 2563	Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	reximdai 2564	Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
Theorem	reximdv2 2565*	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐵 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒))
Theorem	reximdvai 2566*	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 14-Nov-2002.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
Theorem	reximdv 2567*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
Theorem	reximdva 2568*	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
Theorem	reximddv 2569*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 7-Dec-2016.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)
Theorem	reximssdv 2570*	Derivation of a restricted existential quantification over a subset (the second hypothesis implies 𝐴 ⊆ 𝐵), deduction form. (Contributed by AV, 21-Aug-2022.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → 𝑥 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → 𝜒)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)
Theorem	reximddv2 2571*	Double deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)
Theorem	r19.12 2572*	Theorem 19.12 of [Margaris] p. 89 with restricted quantifiers. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
Theorem	r19.23t 2573	Closed theorem form of r19.23 2574. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 8-Oct-2016.)
⊢ (Ⅎ𝑥𝜓 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)))
Theorem	r19.23 2574	Theorem 19.23 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 22-Oct-2010.) (Proof shortened by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))
Theorem	r19.23v 2575*	Theorem 19.23 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 31-Aug-1999.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))
Theorem	rexlimi 2576	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 30-Nov-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)
Theorem	rexlimiv 2577*	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)
Theorem	rexlimiva 2578*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)
Theorem	rexlimivw 2579*	Weaker version of rexlimiv 2577. (Contributed by FL, 19-Sep-2011.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)
Theorem	rexlimd 2580	Deduction from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimd2 2581	Version of rexlimd 2580 with deduction version of second hypothesis. (Contributed by NM, 21-Jul-2013.) (Revised by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimdv 2582*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimdva 2583*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimdvaa 2584*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimdv3a 2585*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 2582. (Contributed by NM, 7-Jun-2015.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimdva2 2586*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimdvw 2587*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Jun-2014.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimddv 2588*	Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	rexlimivv 2589*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓)
Theorem	rexlimdvv 2590*	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))
Theorem	rexlimdvva 2591*	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))
Theorem	r19.26 2592	Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
Theorem	r19.27v 2593*	Restricted quantitifer version of one direction of 19.27 1549. (The other direction holds when 𝐴 is inhabited, see r19.27mv 3505.) (Contributed by NM, 3-Jun-2004.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 17-Jun-2023.)
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
Theorem	r19.28v 2594*	Restricted quantifier version of one direction of 19.28 1551. (The other direction holds when 𝐴 is inhabited, see r19.28mv 3501.) (Contributed by NM, 2-Apr-2004.) (Proof shortened by Wolf Lammen, 17-Jun-2023.)
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
Theorem	r19.26-2 2595	Theorem 19.26 of [Margaris] p. 90 with 2 restricted quantifiers. (Contributed by NM, 10-Aug-2004.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓))
Theorem	r19.26-3 2596	Theorem 19.26 of [Margaris] p. 90 with 3 restricted quantifiers. (Contributed by FL, 22-Nov-2010.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓 ∧ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	r19.26m 2597	Theorem 19.26 of [Margaris] p. 90 with mixed quantifiers. (Contributed by NM, 22-Feb-2004.)
⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜓)) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	ralbi 2598	Distribute a restricted universal quantifier over a biconditional. Theorem 19.15 of [Margaris] p. 90 with restricted quantification. (Contributed by NM, 6-Oct-2003.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓))
Theorem	rexbi 2599	Distribute a restricted existential quantifier over a biconditional. Theorem 19.18 of [Margaris] p. 90 with restricted quantification. (Contributed by Jim Kingdon, 21-Jan-2019.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓))
Theorem	ralbiim 2600	Split a biconditional and distribute quantifier. (Contributed by NM, 3-Jun-2012.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)))