Theorem List for Intuitionistic Logic Explorer - 2401-2500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | r19.21bi 2401 |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 20-Nov-1994.)
|
⊢ (φ
→ ∀x ∈ A ψ) ⇒ ⊢ ((φ ∧
x ∈
A) → ψ) |
|
Theorem | rspec2 2402 |
Specialization rule for restricted quantification. (Contributed by NM,
20-Nov-1994.)
|
⊢ ∀x ∈ A ∀y ∈ B φ ⇒ ⊢ ((x ∈ A ∧ y ∈ B) → φ) |
|
Theorem | rspec3 2403 |
Specialization rule for restricted quantification. (Contributed by NM,
20-Nov-1994.)
|
⊢ ∀x ∈ A ∀y ∈ B ∀z ∈ 𝐶 φ ⇒ ⊢ ((x ∈ A ∧ y ∈ B ∧ z ∈ 𝐶) → φ) |
|
Theorem | r19.21be 2404 |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 21-Nov-1994.)
|
⊢ (φ
→ ∀x ∈ A ψ) ⇒ ⊢ ∀x ∈ A (φ → ψ) |
|
Theorem | nrex 2405 |
Inference adding restricted existential quantifier to negated wff.
(Contributed by NM, 16-Oct-2003.)
|
⊢ (x ∈ A →
¬ ψ)
⇒ ⊢ ¬ ∃x ∈ A ψ |
|
Theorem | nrexdv 2406* |
Deduction adding restricted existential quantifier to negated wff.
(Contributed by NM, 16-Oct-2003.)
|
⊢ ((φ
∧ x ∈ A) →
¬ ψ)
⇒ ⊢ (φ → ¬ ∃x ∈ A ψ) |
|
Theorem | rexim 2407 |
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 2408 |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 10-Feb-1997.)
|
⊢ (x ∈ A →
(φ → ψ)) ⇒ ⊢ (∃x ∈ A φ → ∃x ∈ A ψ) |
|
Theorem | reximi2 2409 |
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 2410 |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 18-Oct-1996.)
|
⊢ (φ
→ ψ)
⇒ ⊢ (∃x ∈ A φ → ∃x ∈ A ψ) |
|
Theorem | reximdai 2411 |
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 2412* |
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 2413* |
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 2414* |
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 2415* |
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 2416* |
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
φ) |
|
Theorem | r19.23t 2417 |
Closed theorem form of r19.23 2418. (Contributed by NM, 4-Mar-2013.)
(Revised by Mario Carneiro, 8-Oct-2016.)
|
⊢ (Ⅎxψ →
(∀x
∈ A
(φ → ψ) ↔ (∃x ∈ A φ → ψ))) |
|
Theorem | r19.23 2418 |
Theorem 19.23 of [Margaris] p. 90 with
restricted quantifiers.
(Contributed by NM, 22-Oct-2010.) (Proof shortened by Mario Carneiro,
8-Oct-2016.)
|
⊢ Ⅎxψ ⇒ ⊢ (∀x ∈ A (φ → ψ) ↔ (∃x ∈ A φ → ψ)) |
|
Theorem | r19.23v 2419* |
Theorem 19.23 of [Margaris] p. 90 with
restricted quantifiers.
(Contributed by NM, 31-Aug-1999.)
|
⊢ (∀x ∈ A (φ →
ψ) ↔ (∃x ∈ A φ → ψ)) |
|
Theorem | rexlimi 2420 |
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.)
|
⊢ Ⅎxψ
& ⊢ (x ∈ A →
(φ → ψ)) ⇒ ⊢ (∃x ∈ A φ → ψ) |
|
Theorem | rexlimiv 2421* |
Inference from Theorem 19.23 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 20-Nov-1994.)
|
⊢ (x ∈ A →
(φ → ψ)) ⇒ ⊢ (∃x ∈ A φ → ψ) |
|
Theorem | rexlimiva 2422* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 18-Dec-2006.)
|
⊢ ((x ∈ A ∧ φ) →
ψ) ⇒ ⊢ (∃x ∈ A φ → ψ) |
|
Theorem | rexlimivw 2423* |
Weaker version of rexlimiv 2421. (Contributed by FL, 19-Sep-2011.)
|
⊢ (φ
→ ψ)
⇒ ⊢ (∃x ∈ A φ → ψ) |
|
Theorem | rexlimd 2424 |
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.)
|
⊢ Ⅎxφ
& ⊢ Ⅎxχ
& ⊢ (φ
→ (x ∈ A →
(ψ → χ))) ⇒ ⊢ (φ → (∃x ∈ A ψ → χ)) |
|
Theorem | rexlimd2 2425 |
Version of rexlimd 2424 with deduction version of second hypothesis.
(Contributed by NM, 21-Jul-2013.) (Revised by Mario Carneiro,
8-Oct-2016.)
|
⊢ Ⅎxφ
& ⊢ (φ
→ Ⅎxχ)
& ⊢ (φ
→ (x ∈ A →
(ψ → χ))) ⇒ ⊢ (φ → (∃x ∈ A ψ → χ)) |
|
Theorem | rexlimdv 2426* |
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.)
|
⊢ (φ
→ (x ∈ A →
(ψ → χ))) ⇒ ⊢ (φ → (∃x ∈ A ψ → χ)) |
|
Theorem | rexlimdva 2427* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 20-Jan-2007.)
|
⊢ ((φ
∧ x ∈ A) →
(ψ → χ)) ⇒ ⊢ (φ → (∃x ∈ A ψ → χ)) |
|
Theorem | rexlimdvaa 2428* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by Mario Carneiro, 15-Jun-2016.)
|
⊢ ((φ
∧ (x
∈ A
∧ ψ))
→ χ)
⇒ ⊢ (φ → (∃x ∈ A ψ → χ)) |
|
Theorem | rexlimdv3a 2429* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). Frequently-used variant of rexlimdv 2426. (Contributed by NM,
7-Jun-2015.)
|
⊢ ((φ
∧ x ∈ A ∧ ψ) →
χ) ⇒ ⊢ (φ → (∃x ∈ A ψ → χ)) |
|
Theorem | rexlimdvw 2430* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 18-Jun-2014.)
|
⊢ (φ
→ (ψ → χ)) ⇒ ⊢ (φ → (∃x ∈ A ψ → χ)) |
|
Theorem | rexlimddv 2431* |
Restricted existential elimination rule of natural deduction.
(Contributed by Mario Carneiro, 15-Jun-2016.)
|
⊢ (φ
→ ∃x ∈ A ψ)
& ⊢ ((φ
∧ (x
∈ A
∧ ψ))
→ χ)
⇒ ⊢ (φ → χ) |
|
Theorem | rexlimivv 2432* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 17-Feb-2004.)
|
⊢ ((x ∈ A ∧ y ∈ B) →
(φ → ψ)) ⇒ ⊢ (∃x ∈ A ∃y ∈ B φ → ψ) |
|
Theorem | rexlimdvv 2433* |
Inference from Theorem 19.23 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 22-Jul-2004.)
|
⊢ (φ
→ ((x ∈ A ∧ y ∈ B) →
(ψ → χ))) ⇒ ⊢ (φ → (∃x ∈ A ∃y ∈ B ψ → χ)) |
|
Theorem | rexlimdvva 2434* |
Inference from Theorem 19.23 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 18-Jun-2014.)
|
⊢ ((φ
∧ (x
∈ A
∧ y ∈ B)) →
(ψ → χ)) ⇒ ⊢ (φ → (∃x ∈ A ∃y ∈ B ψ → χ)) |
|
Theorem | r19.26 2435 |
Theorem 19.26 of [Margaris] p. 90 with
restricted quantifiers.
(Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon,
30-May-2011.)
|
⊢ (∀x ∈ A (φ ∧ ψ) ↔
(∀x
∈ A
φ ∧
∀x
∈ A
ψ)) |
|
Theorem | r19.26-2 2436 |
Theorem 19.26 of [Margaris] p. 90 with 2
restricted quantifiers.
(Contributed by NM, 10-Aug-2004.)
|
⊢ (∀x ∈ A ∀y ∈ B (φ ∧ ψ) ↔
(∀x
∈ A
∀y
∈ B
φ ∧
∀x
∈ A
∀y
∈ B
ψ)) |
|
Theorem | r19.26-3 2437 |
Theorem 19.26 of [Margaris] p. 90 with 3
restricted quantifiers.
(Contributed by FL, 22-Nov-2010.)
|
⊢ (∀x ∈ A (φ ∧ ψ ∧ χ) ↔
(∀x
∈ A
φ ∧
∀x
∈ A
ψ ∧
∀x
∈ A
χ)) |
|
Theorem | r19.26m 2438 |
Theorem 19.26 of [Margaris] p. 90 with mixed
quantifiers. (Contributed by
NM, 22-Feb-2004.)
|
⊢ (∀x((x ∈ A →
φ) ∧
(x ∈
B → ψ)) ↔ (∀x ∈ A φ ∧ ∀x ∈ B ψ)) |
|
Theorem | ralbi 2439 |
Distribute a restricted universal quantifier over a biconditional.
Theorem 19.15 of [Margaris] p. 90 with
restricted quantification.
(Contributed by NM, 6-Oct-2003.)
|
⊢ (∀x ∈ A (φ ↔
ψ) → (∀x ∈ A φ ↔ ∀x ∈ A ψ)) |
|
Theorem | rexbi 2440 |
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.)
|
⊢ (∀x ∈ A (φ ↔
ψ) → (∃x ∈ A φ ↔ ∃x ∈ A ψ)) |
|
Theorem | ralbiim 2441 |
Split a biconditional and distribute quantifier. (Contributed by NM,
3-Jun-2012.)
|
⊢ (∀x ∈ A (φ ↔
ψ) ↔ (∀x ∈ A (φ → ψ) ∧ ∀x ∈ A (ψ → φ))) |
|
Theorem | r19.27av 2442* |
Restricted version of one direction of Theorem 19.27 of [Margaris]
p. 90. (The other direction doesn't hold when A is empty.)
(Contributed by NM, 3-Jun-2004.) (Proof shortened by Andrew Salmon,
30-May-2011.)
|
⊢ ((∀x ∈ A φ ∧ ψ) →
∀x
∈ A
(φ ∧
ψ)) |
|
Theorem | r19.28av 2443* |
Restricted version of one direction of Theorem 19.28 of [Margaris]
p. 90. (The other direction doesn't hold when A is empty.)
(Contributed by NM, 2-Apr-2004.)
|
⊢ ((φ
∧ ∀x ∈ A ψ) → ∀x ∈ A (φ ∧ ψ)) |
|
Theorem | r19.29 2444 |
Theorem 19.29 of [Margaris] p. 90 with
restricted quantifiers.
(Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon,
30-May-2011.)
|
⊢ ((∀x ∈ A φ ∧ ∃x ∈ A ψ) →
∃x
∈ A
(φ ∧
ψ)) |
|
Theorem | r19.29r 2445 |
Variation of Theorem 19.29 of [Margaris] p. 90
with restricted
quantifiers. (Contributed by NM, 31-Aug-1999.)
|
⊢ ((∃x ∈ A φ ∧ ∀x ∈ A ψ) →
∃x
∈ A
(φ ∧
ψ)) |
|
Theorem | r19.29af2 2446 |
A commonly used pattern based on r19.29 2444 (Contributed by Thierry
Arnoux, 17-Dec-2017.)
|
⊢ Ⅎxφ
& ⊢ Ⅎxχ
& ⊢ (((φ
∧ x ∈ A) ∧ ψ) →
χ) & ⊢ (φ → ∃x ∈ A ψ) ⇒ ⊢ (φ → χ) |
|
Theorem | r19.29af 2447* |
A commonly used pattern based on r19.29 2444 (Contributed by Thierry
Arnoux, 29-Nov-2017.)
|
⊢ Ⅎxφ
& ⊢ (((φ
∧ x ∈ A) ∧ ψ) →
χ) & ⊢ (φ → ∃x ∈ A ψ) ⇒ ⊢ (φ → χ) |
|
Theorem | r19.29a 2448* |
A commonly used pattern based on r19.29 2444 (Contributed by Thierry
Arnoux, 22-Nov-2017.)
|
⊢ (((φ
∧ x ∈ A) ∧ ψ) →
χ) & ⊢ (φ → ∃x ∈ A ψ) ⇒ ⊢ (φ → χ) |
|
Theorem | r19.29d2r 2449 |
Theorem 19.29 of [Margaris] p. 90 with two
restricted quantifiers,
deduction version (Contributed by Thierry Arnoux, 30-Jan-2017.)
|
⊢ (φ
→ ∀x ∈ A ∀y ∈ B ψ)
& ⊢ (φ
→ ∃x ∈ A ∃y ∈ B χ) ⇒ ⊢ (φ → ∃x ∈ A ∃y ∈ B (ψ ∧ χ)) |
|
Theorem | r19.29vva 2450* |
A commonly used pattern based on r19.29 2444, version with two restricted
quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.)
|
⊢ ((((φ
∧ x ∈ A) ∧ y ∈ B) ∧ ψ) →
χ) & ⊢ (φ → ∃x ∈ A ∃y ∈ B ψ) ⇒ ⊢ (φ → χ) |
|
Theorem | r19.32r 2451 |
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.)
|
⊢ Ⅎxφ ⇒ ⊢ ((φ ∨ ∀x ∈ A ψ) → ∀x ∈ A (φ ∨ ψ)) |
|
Theorem | r19.32vr 2452* |
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 2453. (Contributed by Jim Kingdon, 19-Aug-2018.)
|
⊢ ((φ
∨ ∀x ∈ A ψ) → ∀x ∈ A (φ ∨ ψ)) |
|
Theorem | r19.32vdc 2453* |
Theorem 19.32 of [Margaris] p. 90 with
restricted quantifiers, where
φ is
decidable. (Contributed by Jim Kingdon, 4-Jun-2018.)
|
⊢ (DECID φ → (∀x ∈ A (φ ∨ ψ) ↔ (φ ∨ ∀x ∈ A ψ))) |
|
Theorem | r19.35-1 2454 |
Restricted quantifier version of 19.35-1 1512. (Contributed by Jim Kingdon,
4-Jun-2018.)
|
⊢ (∃x ∈ A (φ →
ψ) → (∀x ∈ A φ → ∃x ∈ A ψ)) |
|
Theorem | r19.36av 2455* |
One direction of a restricted quantifier version of Theorem 19.36 of
[Margaris] p. 90. In classical logic,
the converse would hold if A
has at least one element, but in intuitionistic logic, that is not a
sufficient condition. (Contributed by NM, 22-Oct-2003.)
|
⊢ (∃x ∈ A (φ →
ψ) → (∀x ∈ A φ → ψ)) |
|
Theorem | r19.37 2456 |
Restricted version of one direction of Theorem 19.37 of [Margaris]
p. 90. In classical logic the converse would hold if A 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.)
|
⊢ Ⅎxφ ⇒ ⊢ (∃x ∈ A (φ → ψ) → (φ → ∃x ∈ A ψ)) |
|
Theorem | r19.37av 2457* |
Restricted version of one direction of Theorem 19.37 of [Margaris]
p. 90. (Contributed by NM, 2-Apr-2004.)
|
⊢ (∃x ∈ A (φ →
ψ) → (φ → ∃x ∈ A ψ)) |
|
Theorem | r19.40 2458 |
Restricted quantifier version of Theorem 19.40 of [Margaris] p. 90.
(Contributed by NM, 2-Apr-2004.)
|
⊢ (∃x ∈ A (φ ∧ ψ) →
(∃x
∈ A
φ ∧
∃x
∈ A
ψ)) |
|
Theorem | r19.41 2459 |
Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
(Contributed by NM, 1-Nov-2010.)
|
⊢ Ⅎxψ ⇒ ⊢ (∃x ∈ A (φ ∧ ψ) ↔ (∃x ∈ A φ ∧ ψ)) |
|
Theorem | r19.41v 2460* |
Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
(Contributed by NM, 17-Dec-2003.)
|
⊢ (∃x ∈ A (φ ∧ ψ) ↔
(∃x
∈ A
φ ∧
ψ)) |
|
Theorem | r19.42v 2461* |
Restricted version of Theorem 19.42 of [Margaris] p. 90. (Contributed
by NM, 27-May-1998.)
|
⊢ (∃x ∈ A (φ ∧ ψ) ↔
(φ ∧
∃x
∈ A
ψ)) |
|
Theorem | r19.43 2462 |
Restricted version of Theorem 19.43 of [Margaris] p. 90. (Contributed by
NM, 27-May-1998.) (Proof rewritten by Jim Kingdon, 5-Jun-2018.)
|
⊢ (∃x ∈ A (φ ∨ ψ) ↔
(∃x
∈ A
φ ∨
∃x
∈ A
ψ)) |
|
Theorem | r19.44av 2463* |
One direction of a restricted quantifier version of Theorem 19.44 of
[Margaris] p. 90. The other direction
doesn't hold when A
is
empty. (Contributed by NM, 2-Apr-2004.)
|
⊢ (∃x ∈ A (φ ∨ ψ) →
(∃x
∈ A
φ ∨
ψ)) |
|
Theorem | r19.45av 2464* |
Restricted version of one direction of Theorem 19.45 of [Margaris]
p. 90. (The other direction doesn't hold when A is empty.)
(Contributed by NM, 2-Apr-2004.)
|
⊢ (∃x ∈ A (φ ∨ ψ) →
(φ ∨
∃x
∈ A
ψ)) |
|
Theorem | ralcomf 2465* |
Commutation of restricted quantifiers. (Contributed by Mario Carneiro,
14-Oct-2016.)
|
⊢ ℲyA & ⊢
ℲxB ⇒ ⊢ (∀x ∈ A ∀y ∈ B φ ↔ ∀y ∈ B ∀x ∈ A φ) |
|
Theorem | rexcomf 2466* |
Commutation of restricted quantifiers. (Contributed by Mario Carneiro,
14-Oct-2016.)
|
⊢ ℲyA & ⊢
ℲxB ⇒ ⊢ (∃x ∈ A ∃y ∈ B φ ↔ ∃y ∈ B ∃x ∈ A φ) |
|
Theorem | ralcom 2467* |
Commutation of restricted quantifiers. (Contributed by NM,
13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
⊢ (∀x ∈ A ∀y ∈ B φ ↔
∀y
∈ B
∀x
∈ A
φ) |
|
Theorem | rexcom 2468* |
Commutation of restricted quantifiers. (Contributed by NM,
19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
⊢ (∃x ∈ A ∃y ∈ B φ ↔
∃y
∈ B
∃x
∈ A
φ) |
|
Theorem | rexcom13 2469* |
Swap 1st and 3rd restricted existential quantifiers. (Contributed by
NM, 8-Apr-2015.)
|
⊢ (∃x ∈ A ∃y ∈ B ∃z ∈ 𝐶 φ ↔ ∃z ∈ 𝐶 ∃y ∈ B ∃x ∈ A φ) |
|
Theorem | rexrot4 2470* |
Rotate existential restricted quantifiers twice. (Contributed by NM,
8-Apr-2015.)
|
⊢ (∃x ∈ A ∃y ∈ B ∃z ∈ 𝐶 ∃w ∈ 𝐷 φ
↔ ∃z ∈ 𝐶 ∃w ∈ 𝐷 ∃x ∈ A ∃y ∈ B φ) |
|
Theorem | ralcom3 2471 |
A commutative law for restricted quantifiers that swaps the domain of
the restriction. (Contributed by NM, 22-Feb-2004.)
|
⊢ (∀x ∈ A (x ∈ B →
φ) ↔ ∀x ∈ B (x ∈ A → φ)) |
|
Theorem | reean 2472* |
Rearrange existential quantifiers. (Contributed by NM, 27-Oct-2010.)
(Proof shortened by Andrew Salmon, 30-May-2011.)
|
⊢ Ⅎyφ
& ⊢ Ⅎxψ ⇒ ⊢ (∃x ∈ A ∃y ∈ B (φ ∧ ψ) ↔ (∃x ∈ A φ ∧ ∃y ∈ B ψ)) |
|
Theorem | reeanv 2473* |
Rearrange existential quantifiers. (Contributed by NM, 9-May-1999.)
|
⊢ (∃x ∈ A ∃y ∈ B (φ ∧ ψ) ↔
(∃x
∈ A
φ ∧
∃y
∈ B
ψ)) |
|
Theorem | 3reeanv 2474* |
Rearrange three existential quantifiers. (Contributed by Jeff Madsen,
11-Jun-2010.)
|
⊢ (∃x ∈ A ∃y ∈ B ∃z ∈ 𝐶 (φ ∧ ψ ∧ χ) ↔ (∃x ∈ A φ ∧ ∃y ∈ B ψ ∧ ∃z ∈ 𝐶 χ)) |
|
Theorem | nfreu1 2475 |
x is not free in
∃!x ∈ Aφ.
(Contributed by NM,
19-Mar-1997.)
|
⊢ Ⅎx∃!x ∈ A φ |
|
Theorem | nfrmo1 2476 |
x is not free in
∃*x ∈ Aφ.
(Contributed by NM,
16-Jun-2017.)
|
⊢ Ⅎx∃*x ∈ A φ |
|
Theorem | nfreudxy 2477* |
Not-free deduction for restricted uniqueness. This is a version where
x and y are distinct.
(Contributed by Jim Kingdon,
6-Jun-2018.)
|
⊢ Ⅎyφ
& ⊢ (φ
→ ℲxA)
& ⊢ (φ
→ Ⅎxψ) ⇒ ⊢ (φ → Ⅎx∃!y ∈ A ψ) |
|
Theorem | nfreuxy 2478* |
Not-free for restricted uniqueness. This is a version where x and
y are
distinct. (Contributed by Jim Kingdon, 6-Jun-2018.)
|
⊢ ℲxA & ⊢
Ⅎxφ ⇒ ⊢ Ⅎx∃!y ∈ A φ |
|
Theorem | rabid 2479 |
An "identity" law of concretion for restricted abstraction. Special
case
of Definition 2.1 of [Quine] p. 16.
(Contributed by NM, 9-Oct-2003.)
|
⊢ (x ∈ {x ∈ A ∣
φ} ↔ (x ∈ A ∧ φ)) |
|
Theorem | rabid2 2480* |
An "identity" law for restricted class abstraction. (Contributed by
NM,
9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|
⊢ (A =
{x ∈
A ∣ φ} ↔ ∀x ∈ A φ) |
|
Theorem | rabbi 2481 |
Equivalent wff's correspond to equal restricted class abstractions.
Closed theorem form of rabbidva 2542. (Contributed by NM,
25-Nov-2013.)
|
⊢ (∀x ∈ A (ψ ↔
χ) ↔ {x ∈ A ∣ ψ} = {x
∈ A
∣ χ}) |
|
Theorem | rabswap 2482 |
Swap with a membership relation in a restricted class abstraction.
(Contributed by NM, 4-Jul-2005.)
|
⊢ {x ∈ A ∣
x ∈
B} = {x ∈ B ∣ x
∈ A} |
|
Theorem | nfrab1 2483 |
The abstraction variable in a restricted class abstraction isn't free.
(Contributed by NM, 19-Mar-1997.)
|
⊢ Ⅎx{x ∈ A ∣
φ} |
|
Theorem | nfrabxy 2484* |
A variable not free in a wff remains so in a restricted class
abstraction. (Contributed by Jim Kingdon, 19-Jul-2018.)
|
⊢ Ⅎxφ
& ⊢ ℲxA ⇒ ⊢ Ⅎx{y ∈ A ∣
φ} |
|
Theorem | reubida 2485 |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by Mario Carneiro, 19-Nov-2016.)
|
⊢ Ⅎxφ
& ⊢ ((φ
∧ x ∈ A) →
(ψ ↔ χ)) ⇒ ⊢ (φ → (∃!x ∈ A ψ ↔ ∃!x ∈ A χ)) |
|
Theorem | reubidva 2486* |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 13-Nov-2004.)
|
⊢ ((φ
∧ x ∈ A) →
(ψ ↔ χ)) ⇒ ⊢ (φ → (∃!x ∈ A ψ ↔ ∃!x ∈ A χ)) |
|
Theorem | reubidv 2487* |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 17-Oct-1996.)
|
⊢ (φ
→ (ψ ↔ χ)) ⇒ ⊢ (φ → (∃!x ∈ A ψ ↔ ∃!x ∈ A χ)) |
|
Theorem | reubiia 2488 |
Formula-building rule for restricted existential quantifier (inference
rule). (Contributed by NM, 14-Nov-2004.)
|
⊢ (x ∈ A →
(φ ↔ ψ)) ⇒ ⊢ (∃!x ∈ A φ ↔ ∃!x ∈ A ψ) |
|
Theorem | reubii 2489 |
Formula-building rule for restricted existential quantifier (inference
rule). (Contributed by NM, 22-Oct-1999.)
|
⊢ (φ
↔ ψ)
⇒ ⊢ (∃!x ∈ A φ ↔ ∃!x ∈ A ψ) |
|
Theorem | rmobida 2490 |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 16-Jun-2017.)
|
⊢ Ⅎxφ
& ⊢ ((φ
∧ x ∈ A) →
(ψ ↔ χ)) ⇒ ⊢ (φ → (∃*x ∈ A ψ ↔ ∃*x ∈ A χ)) |
|
Theorem | rmobidva 2491* |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 16-Jun-2017.)
|
⊢ ((φ
∧ x ∈ A) →
(ψ ↔ χ)) ⇒ ⊢ (φ → (∃*x ∈ A ψ ↔ ∃*x ∈ A χ)) |
|
Theorem | rmobidv 2492* |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 16-Jun-2017.)
|
⊢ (φ
→ (ψ ↔ χ)) ⇒ ⊢ (φ → (∃*x ∈ A ψ ↔ ∃*x ∈ A χ)) |
|
Theorem | rmobiia 2493 |
Formula-building rule for restricted existential quantifier (inference
rule). (Contributed by NM, 16-Jun-2017.)
|
⊢ (x ∈ A →
(φ ↔ ψ)) ⇒ ⊢ (∃*x ∈ A φ ↔ ∃*x ∈ A ψ) |
|
Theorem | rmobii 2494 |
Formula-building rule for restricted existential quantifier (inference
rule). (Contributed by NM, 16-Jun-2017.)
|
⊢ (φ
↔ ψ)
⇒ ⊢ (∃*x ∈ A φ ↔ ∃*x ∈ A ψ) |
|
Theorem | raleqf 2495 |
Equality theorem for restricted universal quantifier, with
bound-variable hypotheses instead of distinct variable restrictions.
(Contributed by NM, 7-Mar-2004.) (Revised by Andrew Salmon,
11-Jul-2011.)
|
⊢ ℲxA & ⊢
ℲxB ⇒ ⊢ (A = B →
(∀x
∈ A
φ ↔ ∀x ∈ B φ)) |
|
Theorem | rexeqf 2496 |
Equality theorem for restricted existential quantifier, with
bound-variable hypotheses instead of distinct variable restrictions.
(Contributed by NM, 9-Oct-2003.) (Revised by Andrew Salmon,
11-Jul-2011.)
|
⊢ ℲxA & ⊢
ℲxB ⇒ ⊢ (A = B →
(∃x
∈ A
φ ↔ ∃x ∈ B φ)) |
|
Theorem | reueq1f 2497 |
Equality theorem for restricted uniqueness quantifier, with
bound-variable hypotheses instead of distinct variable restrictions.
(Contributed by NM, 5-Apr-2004.) (Revised by Andrew Salmon,
11-Jul-2011.)
|
⊢ ℲxA & ⊢
ℲxB ⇒ ⊢ (A = B →
(∃!x
∈ A
φ ↔ ∃!x ∈ B φ)) |
|
Theorem | rmoeq1f 2498 |
Equality theorem for restricted uniqueness quantifier, with
bound-variable hypotheses instead of distinct variable restrictions.
(Contributed by Alexander van der Vekens, 17-Jun-2017.)
|
⊢ ℲxA & ⊢
ℲxB ⇒ ⊢ (A = B →
(∃*x
∈ A
φ ↔ ∃*x ∈ B φ)) |
|
Theorem | raleq 2499* |
Equality theorem for restricted universal quantifier. (Contributed by
NM, 16-Nov-1995.)
|
⊢ (A =
B → (∀x ∈ A φ ↔ ∀x ∈ B φ)) |
|
Theorem | rexeq 2500* |
Equality theorem for restricted existential quantifier. (Contributed by
NM, 29-Oct-1995.)
|
⊢ (A =
B → (∃x ∈ A φ ↔ ∃x ∈ B φ)) |