Theorem List for Intuitionistic Logic Explorer - 2501-2600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ralimdaa 2501 |
Deduction quantifying both antecedent and consequent, based on Theorem
19.20 of [Margaris] p. 90.
(Contributed by NM, 22-Sep-2003.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | ralimdva 2502* |
Deduction quantifying both antecedent and consequent, based on Theorem
19.20 of [Margaris] p. 90.
(Contributed by NM, 22-May-1999.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | ralimdv 2503* |
Deduction quantifying both antecedent and consequent, based on Theorem
19.20 of [Margaris] p. 90.
(Contributed by NM, 8-Oct-2003.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | ralimdvva 2504* |
Deduction doubly quantifying both antecedent and consequent, based on
Theorem 19.20 of [Margaris] p. 90 (alim 1434). (Contributed by AV,
27-Nov-2019.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
|
Theorem | ralimdv2 2505* |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 1-Feb-2005.)
|
⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐵 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒)) |
|
Theorem | ralrimi 2506 |
Inference from Theorem 19.21 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 10-Oct-1999.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
|
Theorem | ralrimiv 2507* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 22-Nov-1994.)
|
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
|
Theorem | ralrimiva 2508* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 2-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
|
Theorem | ralrimivw 2509* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 18-Jun-2014.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
|
Theorem | r19.21t 2510 |
Theorem 19.21 of [Margaris] p. 90 with
restricted quantifiers (closed
theorem version). (Contributed by NM, 1-Mar-2008.)
|
⊢ (Ⅎ𝑥𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))) |
|
Theorem | r19.21 2511 |
Theorem 19.21 of [Margaris] p. 90 with
restricted quantifiers.
(Contributed by Scott Fenton, 30-Mar-2011.)
|
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.21v 2512* |
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 2513 |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 16-Feb-2004.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | ralrimdv 2514* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 27-May-1998.)
|
⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | ralrimdva 2515* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 2-Feb-2008.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | ralrimivv 2516* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version with double quantification.) (Contributed by NM,
24-Jul-2004.)
|
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
|
Theorem | ralrimivva 2517* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version with double quantification.) (Contributed by Jeff
Madsen, 19-Jun-2011.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
|
Theorem | ralrimivvva 2518* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version with triple quantification.) (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
|
Theorem | ralrimdvv 2519* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version with double quantification.) (Contributed by NM,
1-Jun-2005.)
|
⊢ (𝜑 → (𝜓 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
|
Theorem | ralrimdvva 2520* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version with double quantification.) (Contributed by NM,
2-Feb-2008.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
|
Theorem | rgen2 2521* |
Generalization rule for restricted quantification. (Contributed by NM,
30-May-1999.)
|
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 |
|
Theorem | rgen3 2522* |
Generalization rule for restricted quantification. (Contributed by NM,
12-Jan-2008.)
|
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑) ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 |
|
Theorem | r19.21bi 2523 |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 20-Nov-1994.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) |
|
Theorem | rspec2 2524 |
Specialization rule for restricted quantification. (Contributed by NM,
20-Nov-1994.)
|
⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) |
|
Theorem | rspec3 2525 |
Specialization rule for restricted quantification. (Contributed by NM,
20-Nov-1994.)
|
⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑) |
|
Theorem | r19.21be 2526 |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 21-Nov-1994.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) |
|
Theorem | nrex 2527 |
Inference adding restricted existential quantifier to negated wff.
(Contributed by NM, 16-Oct-2003.)
|
⊢ (𝑥 ∈ 𝐴 → ¬ 𝜓) ⇒ ⊢ ¬ ∃𝑥 ∈ 𝐴 𝜓 |
|
Theorem | nrexdv 2528* |
Deduction adding restricted existential quantifier to negated wff.
(Contributed by NM, 16-Oct-2003.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ ∃𝑥 ∈ 𝐴 𝜓) |
|
Theorem | rexim 2529 |
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 2530 |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 10-Feb-1997.)
|
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) |
|
Theorem | reximi2 2531 |
Inference quantifying both antecedent and consequent, based on Theorem
19.22 of [Margaris] p. 90.
(Contributed by NM, 8-Nov-2004.)
|
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
|
Theorem | reximi 2532 |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 18-Oct-1996.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) |
|
Theorem | reximdai 2533 |
Deduction from Theorem 19.22 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 31-Aug-1999.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | reximdv2 2534* |
Deduction quantifying both antecedent and consequent, based on Theorem
19.22 of [Margaris] p. 90.
(Contributed by NM, 17-Sep-2003.)
|
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒)) |
|
Theorem | reximdvai 2535* |
Deduction quantifying both antecedent and consequent, based on Theorem
19.22 of [Margaris] p. 90.
(Contributed by NM, 14-Nov-2002.)
|
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | reximdv 2536* |
Deduction from Theorem 19.22 of [Margaris] p.
90. (Restricted
quantifier version with strong hypothesis.) (Contributed by NM,
24-Jun-1998.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | reximdva 2537* |
Deduction quantifying both antecedent and consequent, based on Theorem
19.22 of [Margaris] p. 90.
(Contributed by NM, 22-May-1999.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | reximddv 2538* |
Deduction from Theorem 19.22 of [Margaris] p.
90. (Contributed by
Thierry Arnoux, 7-Dec-2016.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)
& ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) |
|
Theorem | reximssdv 2539* |
Derivation of a restricted existential quantification over a subset (the
second hypothesis implies 𝐴 ⊆ 𝐵), deduction form. (Contributed by
AV, 21-Aug-2022.)
|
⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → 𝑥 ∈ 𝐴)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) |
|
Theorem | reximddv2 2540* |
Double deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed
by Thierry Arnoux, 15-Dec-2019.)
|
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)
& ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) |
|
Theorem | r19.12 2541* |
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 2542 |
Closed theorem form of r19.23 2543. (Contributed by NM, 4-Mar-2013.)
(Revised by Mario Carneiro, 8-Oct-2016.)
|
⊢ (Ⅎ𝑥𝜓 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))) |
|
Theorem | r19.23 2543 |
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 2544* |
Theorem 19.23 of [Margaris] p. 90 with
restricted quantifiers.
(Contributed by NM, 31-Aug-1999.)
|
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) |
|
Theorem | rexlimi 2545 |
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 2546* |
Inference from Theorem 19.23 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 20-Nov-1994.)
|
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
|
Theorem | rexlimiva 2547* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 18-Dec-2006.)
|
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
|
Theorem | rexlimivw 2548* |
Weaker version of rexlimiv 2546. (Contributed by FL, 19-Sep-2011.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
|
Theorem | rexlimd 2549 |
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 2550 |
Version of rexlimd 2549 with deduction version of second hypothesis.
(Contributed by NM, 21-Jul-2013.) (Revised by Mario Carneiro,
8-Oct-2016.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ (𝜑 → Ⅎ𝑥𝜒)
& ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimdv 2551* |
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 2552* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 20-Jan-2007.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimdvaa 2553* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by Mario Carneiro, 15-Jun-2016.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimdv3a 2554* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). Frequently-used variant of rexlimdv 2551. (Contributed by NM,
7-Jun-2015.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimdva2 2555* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimdvw 2556* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 18-Jun-2014.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimddv 2557* |
Restricted existential elimination rule of natural deduction.
(Contributed by Mario Carneiro, 15-Jun-2016.)
|
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | rexlimivv 2558* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 17-Feb-2004.)
|
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓) |
|
Theorem | rexlimdvv 2559* |
Inference from Theorem 19.23 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 22-Jul-2004.)
|
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) |
|
Theorem | rexlimdvva 2560* |
Inference from Theorem 19.23 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 18-Jun-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) |
|
Theorem | r19.26 2561 |
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 2562* |
Restricted quantitifer version of one direction of 19.27 1541. (The other
direction holds when 𝐴 is inhabited, see r19.27mv 3464.) (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 2563* |
Restricted quantifier version of one direction of 19.28 1543. (The other
direction holds when 𝐴 is inhabited, see r19.28mv 3460.) (Contributed
by NM, 2-Apr-2004.) (Proof shortened by Wolf Lammen, 17-Jun-2023.)
|
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
|
Theorem | r19.26-2 2564 |
Theorem 19.26 of [Margaris] p. 90 with 2
restricted quantifiers.
(Contributed by NM, 10-Aug-2004.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) |
|
Theorem | r19.26-3 2565 |
Theorem 19.26 of [Margaris] p. 90 with 3
restricted quantifiers.
(Contributed by FL, 22-Nov-2010.)
|
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓 ∧ ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | r19.26m 2566 |
Theorem 19.26 of [Margaris] p. 90 with mixed
quantifiers. (Contributed by
NM, 22-Feb-2004.)
|
⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜓)) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | ralbi 2567 |
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 2568 |
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 2569 |
Split a biconditional and distribute quantifier. (Contributed by NM,
3-Jun-2012.)
|
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑))) |
|
Theorem | r19.27av 2570* |
Restricted version of one direction of Theorem 19.27 of [Margaris]
p. 90. (The other direction doesn't hold when 𝐴 is empty.)
(Contributed by NM, 3-Jun-2004.) (Proof shortened by Andrew Salmon,
30-May-2011.)
|
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
|
Theorem | r19.28av 2571* |
Restricted version of one direction of Theorem 19.28 of [Margaris]
p. 90. (The other direction doesn't hold when 𝐴 is empty.)
(Contributed by NM, 2-Apr-2004.)
|
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
|
Theorem | r19.29 2572 |
Theorem 19.29 of [Margaris] p. 90 with
restricted quantifiers.
(Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon,
30-May-2011.)
|
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
|
Theorem | r19.29r 2573 |
Variation of Theorem 19.29 of [Margaris] p. 90
with restricted
quantifiers. (Contributed by NM, 31-Aug-1999.)
|
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
|
Theorem | ralnex2 2574 |
Relationship between two restricted universal and existential quantifiers.
(Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf
Lammen, 18-May-2023.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) |
|
Theorem | r19.29af2 2575 |
A commonly used pattern based on r19.29 2572 (Contributed by Thierry
Arnoux, 17-Dec-2017.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ Ⅎ𝑥𝜒
& ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
& ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | r19.29af 2576* |
A commonly used pattern based on r19.29 2572 (Contributed by Thierry
Arnoux, 29-Nov-2017.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
& ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | r19.29an 2577* |
A commonly used pattern based on r19.29 2572. (Contributed by Thierry
Arnoux, 29-Dec-2019.)
|
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → 𝜒) |
|
Theorem | r19.29a 2578* |
A commonly used pattern based on r19.29 2572 (Contributed by Thierry
Arnoux, 22-Nov-2017.)
|
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
& ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | r19.29d2r 2579 |
Theorem 19.29 of [Margaris] p. 90 with two
restricted quantifiers,
deduction version (Contributed by Thierry Arnoux, 30-Jan-2017.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)
& ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜓 ∧ 𝜒)) |
|
Theorem | r19.29vva 2580* |
A commonly used pattern based on r19.29 2572, version with two restricted
quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.)
|
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)
& ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | r19.32r 2581 |
One direction of Theorem 19.32 of [Margaris]
p. 90 with restricted
quantifiers. For decidable propositions this is an equivalence.
(Contributed by Jim Kingdon, 19-Aug-2018.)
|
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ((𝜑 ∨ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓)) |
|
Theorem | r19.32vr 2582* |
One direction of Theorem 19.32 of [Margaris]
p. 90 with restricted
quantifiers. For decidable propositions this is an equivalence, as seen
at r19.32vdc 2583. (Contributed by Jim Kingdon, 19-Aug-2018.)
|
⊢ ((𝜑 ∨ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓)) |
|
Theorem | r19.32vdc 2583* |
Theorem 19.32 of [Margaris] p. 90 with
restricted quantifiers, where
𝜑 is decidable. (Contributed by Jim
Kingdon, 4-Jun-2018.)
|
⊢ (DECID 𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥 ∈ 𝐴 𝜓))) |
|
Theorem | r19.35-1 2584 |
Restricted quantifier version of 19.35-1 1604. (Contributed by Jim Kingdon,
4-Jun-2018.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.36av 2585* |
One direction of a restricted quantifier version of Theorem 19.36 of
[Margaris] p. 90. In classical logic,
the converse would hold if 𝐴
has at least one element, but in intuitionistic logic, that is not a
sufficient condition. (Contributed by NM, 22-Oct-2003.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → 𝜓)) |
|
Theorem | r19.37 2586 |
Restricted version of one direction of Theorem 19.37 of [Margaris]
p. 90. In classical logic the converse would hold if 𝐴 has at
least
one element, but that is not sufficient in intuitionistic logic.
(Contributed by FL, 13-May-2012.) (Revised by Mario Carneiro,
11-Dec-2016.)
|
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.37av 2587* |
Restricted version of one direction of Theorem 19.37 of [Margaris]
p. 90. (Contributed by NM, 2-Apr-2004.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.40 2588 |
Restricted quantifier version of Theorem 19.40 of [Margaris] p. 90.
(Contributed by NM, 2-Apr-2004.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.41 2589 |
Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
(Contributed by NM, 1-Nov-2010.)
|
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) |
|
Theorem | r19.41v 2590* |
Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
(Contributed by NM, 17-Dec-2003.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) |
|
Theorem | r19.42v 2591* |
Restricted version of Theorem 19.42 of [Margaris] p. 90. (Contributed
by NM, 27-May-1998.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.43 2592 |
Restricted version of Theorem 19.43 of [Margaris] p. 90. (Contributed by
NM, 27-May-1998.) (Proof rewritten by Jim Kingdon, 5-Jun-2018.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.44av 2593* |
One direction of a restricted quantifier version of Theorem 19.44 of
[Margaris] p. 90. The other direction
doesn't hold when 𝐴 is empty.
(Contributed by NM, 2-Apr-2004.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ∨ 𝜓)) |
|
Theorem | r19.45av 2594* |
Restricted version of one direction of Theorem 19.45 of [Margaris]
p. 90. (The other direction doesn't hold when 𝐴 is empty.)
(Contributed by NM, 2-Apr-2004.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | ralcomf 2595* |
Commutation of restricted quantifiers. (Contributed by Mario Carneiro,
14-Oct-2016.)
|
⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rexcomf 2596* |
Commutation of restricted quantifiers. (Contributed by Mario Carneiro,
14-Oct-2016.)
|
⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
|
Theorem | ralcom 2597* |
Commutation of restricted quantifiers. (Contributed by NM,
13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rexcom 2598* |
Commutation of restricted quantifiers. (Contributed by NM,
19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rexcom13 2599* |
Swap 1st and 3rd restricted existential quantifiers. (Contributed by
NM, 8-Apr-2015.)
|
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜑 ↔ ∃𝑧 ∈ 𝐶 ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rexrot4 2600* |
Rotate existential restricted quantifiers twice. (Contributed by NM,
8-Apr-2015.)
|
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 𝜑 ↔ ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) |