Theorem List for Intuitionistic Logic Explorer - 2401-2500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ralinexa 2401 |
A transformation of restricted quantifiers and logical connectives.
(Contributed by NM, 4-Sep-2005.)
|
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
|
Theorem | risset 2402* |
Two ways to say "𝐴 belongs to 𝐵." (Contributed by
NM,
22-Nov-1994.)
|
⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴) |
|
Theorem | hbral 2403 |
Bound-variable hypothesis builder for restricted quantification.
(Contributed by NM, 1-Sep-1999.) (Revised by David Abernethy,
13-Dec-2009.)
|
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
& ⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (∀𝑦 ∈ 𝐴 𝜑 → ∀𝑥∀𝑦 ∈ 𝐴 𝜑) |
|
Theorem | hbra1 2404 |
𝑥
is not free in ∀𝑥 ∈ 𝐴𝜑. (Contributed by NM,
18-Oct-1996.)
|
⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥∀𝑥 ∈ 𝐴 𝜑) |
|
Theorem | nfra1 2405 |
𝑥
is not free in ∀𝑥 ∈ 𝐴𝜑. (Contributed by NM, 18-Oct-1996.)
(Revised by Mario Carneiro, 7-Oct-2016.)
|
⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑 |
|
Theorem | nfraldxy 2406* |
Not-free for restricted universal quantification where 𝑥 and 𝑦
are distinct. See nfraldya 2408 for a version with 𝑦 and
𝐴
distinct instead. (Contributed by Jim Kingdon, 29-May-2018.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜓) |
|
Theorem | nfrexdxy 2407* |
Not-free for restricted existential quantification where 𝑥 and 𝑦
are distinct. See nfrexdya 2409 for a version with 𝑦 and
𝐴
distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜓) |
|
Theorem | nfraldya 2408* |
Not-free for restricted universal quantification where 𝑦 and 𝐴
are distinct. See nfraldxy 2406 for a version with 𝑥 and
𝑦
distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜓) |
|
Theorem | nfrexdya 2409* |
Not-free for restricted existential quantification where 𝑦 and 𝐴
are distinct. See nfrexdxy 2407 for a version with 𝑥 and
𝑦
distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜓) |
|
Theorem | nfralxy 2410* |
Not-free for restricted universal quantification where 𝑥 and 𝑦
are distinct. See nfralya 2412 for a version with 𝑦 and 𝐴
distinct
instead. (Contributed by Jim Kingdon, 30-May-2018.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑 |
|
Theorem | nfrexxy 2411* |
Not-free for restricted existential quantification where 𝑥 and 𝑦
are distinct. See nfrexya 2413 for a version with 𝑦 and 𝐴
distinct
instead. (Contributed by Jim Kingdon, 30-May-2018.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑 |
|
Theorem | nfralya 2412* |
Not-free for restricted universal quantification where 𝑦 and 𝐴
are distinct. See nfralxy 2410 for a version with 𝑥 and 𝑦
distinct
instead. (Contributed by Jim Kingdon, 3-Jun-2018.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑 |
|
Theorem | nfrexya 2413* |
Not-free for restricted existential quantification where 𝑦 and 𝐴
are distinct. See nfrexxy 2411 for a version with 𝑥 and 𝑦
distinct
instead. (Contributed by Jim Kingdon, 3-Jun-2018.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑 |
|
Theorem | nfra2xy 2414* |
Not-free given two restricted quantifiers. (Contributed by Jim Kingdon,
20-Aug-2018.)
|
⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 |
|
Theorem | nfre1 2415 |
𝑥
is not free in ∃𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.)
(Revised by Mario Carneiro, 7-Oct-2016.)
|
⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑 |
|
Theorem | r3al 2416* |
Triple restricted universal quantification. (Contributed by NM,
19-Nov-1995.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑)) |
|
Theorem | alral 2417 |
Universal quantification implies restricted quantification. (Contributed
by NM, 20-Oct-2006.)
|
⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rexex 2418 |
Restricted existence implies existence. (Contributed by NM,
11-Nov-1995.)
|
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥𝜑) |
|
Theorem | rsp 2419 |
Restricted specialization. (Contributed by NM, 17-Oct-1996.)
|
⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑)) |
|
Theorem | rspe 2420 |
Restricted specialization. (Contributed by NM, 12-Oct-1999.)
|
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rsp2 2421 |
Restricted specialization. (Contributed by NM, 11-Feb-1997.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) |
|
Theorem | rsp2e 2422 |
Restricted specialization. (Contributed by FL, 4-Jun-2012.)
|
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) |
|
Theorem | rspec 2423 |
Specialization rule for restricted quantification. (Contributed by NM,
19-Nov-1994.)
|
⊢ ∀𝑥 ∈ 𝐴 𝜑 ⇒ ⊢ (𝑥 ∈ 𝐴 → 𝜑) |
|
Theorem | rgen 2424 |
Generalization rule for restricted quantification. (Contributed by NM,
19-Nov-1994.)
|
⊢ (𝑥 ∈ 𝐴 → 𝜑) ⇒ ⊢ ∀𝑥 ∈ 𝐴 𝜑 |
|
Theorem | rgen2a 2425* |
Generalization rule for restricted quantification. Note that 𝑥 and
𝑦 needn't be distinct (and illustrates
the use of dvelimor 1939).
(Contributed by NM, 23-Nov-1994.) (Proof rewritten by Jim Kingdon,
1-Jun-2018.)
|
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝜑) ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 |
|
Theorem | rgenw 2426 |
Generalization rule for restricted quantification. (Contributed by NM,
18-Jun-2014.)
|
⊢ 𝜑 ⇒ ⊢ ∀𝑥 ∈ 𝐴 𝜑 |
|
Theorem | rgen2w 2427 |
Generalization rule for restricted quantification. Note that 𝑥 and
𝑦 needn't be distinct. (Contributed by
NM, 18-Jun-2014.)
|
⊢ 𝜑 ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 |
|
Theorem | mprg 2428 |
Modus ponens combined with restricted generalization. (Contributed by
NM, 10-Aug-2004.)
|
⊢ (∀𝑥 ∈ 𝐴 𝜑 → 𝜓)
& ⊢ (𝑥 ∈ 𝐴 → 𝜑) ⇒ ⊢ 𝜓 |
|
Theorem | mprgbir 2429 |
Modus ponens on biconditional combined with restricted generalization.
(Contributed by NM, 21-Mar-2004.)
|
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)
& ⊢ (𝑥 ∈ 𝐴 → 𝜓) ⇒ ⊢ 𝜑 |
|
Theorem | ralim 2430 |
Distribution of restricted quantification over implication. (Contributed
by NM, 9-Feb-1997.)
|
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | ralimi2 2431 |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 22-Feb-2004.)
|
⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐵 → 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓) |
|
Theorem | ralimia 2432 |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 19-Jul-1996.)
|
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
|
Theorem | ralimiaa 2433 |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 4-Aug-2007.)
|
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
|
Theorem | ralimi 2434 |
Inference quantifying both antecedent and consequent, with strong
hypothesis. (Contributed by NM, 4-Mar-1997.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
|
Theorem | ral2imi 2435 |
Inference quantifying antecedent, nested antecedent, and consequent,
with a strong hypothesis. (Contributed by NM, 19-Dec-2006.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | ralimdaa 2436 |
Deduction quantifying both antecedent and consequent, based on Theorem
19.20 of [Margaris] p. 90.
(Contributed by NM, 22-Sep-2003.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | ralimdva 2437* |
Deduction quantifying both antecedent and consequent, based on Theorem
19.20 of [Margaris] p. 90.
(Contributed by NM, 22-May-1999.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | ralimdv 2438* |
Deduction quantifying both antecedent and consequent, based on Theorem
19.20 of [Margaris] p. 90.
(Contributed by NM, 8-Oct-2003.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | ralimdv2 2439* |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 1-Feb-2005.)
|
⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐵 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒)) |
|
Theorem | ralrimi 2440 |
Inference from Theorem 19.21 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 10-Oct-1999.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
|
Theorem | ralrimiv 2441* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 22-Nov-1994.)
|
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
|
Theorem | ralrimiva 2442* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 2-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
|
Theorem | ralrimivw 2443* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 18-Jun-2014.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
|
Theorem | r19.21t 2444 |
Theorem 19.21 of [Margaris] p. 90 with
restricted quantifiers (closed
theorem version). (Contributed by NM, 1-Mar-2008.)
|
⊢ (Ⅎ𝑥𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))) |
|
Theorem | r19.21 2445 |
Theorem 19.21 of [Margaris] p. 90 with
restricted quantifiers.
(Contributed by Scott Fenton, 30-Mar-2011.)
|
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.21v 2446* |
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 2447 |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 16-Feb-2004.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | ralrimdv 2448* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 27-May-1998.)
|
⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | ralrimdva 2449* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 2-Feb-2008.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | ralrimivv 2450* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version with double quantification.) (Contributed by NM,
24-Jul-2004.)
|
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
|
Theorem | ralrimivva 2451* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version with double quantification.) (Contributed by Jeff
Madsen, 19-Jun-2011.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
|
Theorem | ralrimivvva 2452* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version with triple quantification.) (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
|
Theorem | ralrimdvv 2453* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version with double quantification.) (Contributed by NM,
1-Jun-2005.)
|
⊢ (𝜑 → (𝜓 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
|
Theorem | ralrimdvva 2454* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version with double quantification.) (Contributed by NM,
2-Feb-2008.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
|
Theorem | rgen2 2455* |
Generalization rule for restricted quantification. (Contributed by NM,
30-May-1999.)
|
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 |
|
Theorem | rgen3 2456* |
Generalization rule for restricted quantification. (Contributed by NM,
12-Jan-2008.)
|
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑) ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 |
|
Theorem | r19.21bi 2457 |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 20-Nov-1994.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) |
|
Theorem | rspec2 2458 |
Specialization rule for restricted quantification. (Contributed by NM,
20-Nov-1994.)
|
⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) |
|
Theorem | rspec3 2459 |
Specialization rule for restricted quantification. (Contributed by NM,
20-Nov-1994.)
|
⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑) |
|
Theorem | r19.21be 2460 |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 21-Nov-1994.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) |
|
Theorem | nrex 2461 |
Inference adding restricted existential quantifier to negated wff.
(Contributed by NM, 16-Oct-2003.)
|
⊢ (𝑥 ∈ 𝐴 → ¬ 𝜓) ⇒ ⊢ ¬ ∃𝑥 ∈ 𝐴 𝜓 |
|
Theorem | nrexdv 2462* |
Deduction adding restricted existential quantifier to negated wff.
(Contributed by NM, 16-Oct-2003.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ ∃𝑥 ∈ 𝐴 𝜓) |
|
Theorem | rexim 2463 |
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 2464 |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 10-Feb-1997.)
|
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) |
|
Theorem | reximi2 2465 |
Inference quantifying both antecedent and consequent, based on Theorem
19.22 of [Margaris] p. 90.
(Contributed by NM, 8-Nov-2004.)
|
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
|
Theorem | reximi 2466 |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 18-Oct-1996.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) |
|
Theorem | reximdai 2467 |
Deduction from Theorem 19.22 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 31-Aug-1999.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | reximdv2 2468* |
Deduction quantifying both antecedent and consequent, based on Theorem
19.22 of [Margaris] p. 90.
(Contributed by NM, 17-Sep-2003.)
|
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒)) |
|
Theorem | reximdvai 2469* |
Deduction quantifying both antecedent and consequent, based on Theorem
19.22 of [Margaris] p. 90.
(Contributed by NM, 14-Nov-2002.)
|
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | reximdv 2470* |
Deduction from Theorem 19.22 of [Margaris] p.
90. (Restricted
quantifier version with strong hypothesis.) (Contributed by NM,
24-Jun-1998.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | reximdva 2471* |
Deduction quantifying both antecedent and consequent, based on Theorem
19.22 of [Margaris] p. 90.
(Contributed by NM, 22-May-1999.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | reximddv 2472* |
Deduction from Theorem 19.22 of [Margaris] p.
90. (Contributed by
Thierry Arnoux, 7-Dec-2016.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)
& ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) |
|
Theorem | reximddv2 2473* |
Double deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed
by Thierry Arnoux, 15-Dec-2019.)
|
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)
& ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) |
|
Theorem | r19.12 2474* |
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 2475 |
Closed theorem form of r19.23 2476. (Contributed by NM, 4-Mar-2013.)
(Revised by Mario Carneiro, 8-Oct-2016.)
|
⊢ (Ⅎ𝑥𝜓 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))) |
|
Theorem | r19.23 2476 |
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 2477* |
Theorem 19.23 of [Margaris] p. 90 with
restricted quantifiers.
(Contributed by NM, 31-Aug-1999.)
|
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) |
|
Theorem | rexlimi 2478 |
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 2479* |
Inference from Theorem 19.23 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 20-Nov-1994.)
|
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
|
Theorem | rexlimiva 2480* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 18-Dec-2006.)
|
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
|
Theorem | rexlimivw 2481* |
Weaker version of rexlimiv 2479. (Contributed by FL, 19-Sep-2011.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
|
Theorem | rexlimd 2482 |
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 2483 |
Version of rexlimd 2482 with deduction version of second hypothesis.
(Contributed by NM, 21-Jul-2013.) (Revised by Mario Carneiro,
8-Oct-2016.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ (𝜑 → Ⅎ𝑥𝜒)
& ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimdv 2484* |
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 2485* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 20-Jan-2007.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimdvaa 2486* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by Mario Carneiro, 15-Jun-2016.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimdv3a 2487* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). Frequently-used variant of rexlimdv 2484. (Contributed by NM,
7-Jun-2015.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimdvw 2488* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 18-Jun-2014.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimddv 2489* |
Restricted existential elimination rule of natural deduction.
(Contributed by Mario Carneiro, 15-Jun-2016.)
|
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | rexlimivv 2490* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 17-Feb-2004.)
|
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓) |
|
Theorem | rexlimdvv 2491* |
Inference from Theorem 19.23 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 22-Jul-2004.)
|
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) |
|
Theorem | rexlimdvva 2492* |
Inference from Theorem 19.23 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 18-Jun-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) |
|
Theorem | r19.26 2493 |
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.26-2 2494 |
Theorem 19.26 of [Margaris] p. 90 with 2
restricted quantifiers.
(Contributed by NM, 10-Aug-2004.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) |
|
Theorem | r19.26-3 2495 |
Theorem 19.26 of [Margaris] p. 90 with 3
restricted quantifiers.
(Contributed by FL, 22-Nov-2010.)
|
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓 ∧ ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | r19.26m 2496 |
Theorem 19.26 of [Margaris] p. 90 with mixed
quantifiers. (Contributed by
NM, 22-Feb-2004.)
|
⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜓)) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | ralbi 2497 |
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 2498 |
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 2499 |
Split a biconditional and distribute quantifier. (Contributed by NM,
3-Jun-2012.)
|
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑))) |
|
Theorem | r19.27av 2500* |
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.)
|
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |