Theorem List for Intuitionistic Logic Explorer - 2301-2400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Syntax | wrex 2301 |
Extend wff notation to include restricted existential quantification.
|
wff ∃x ∈ A φ |
|
Syntax | wreu 2302 |
Extend wff notation to include restricted existential uniqueness.
|
wff ∃!x ∈ A φ |
|
Syntax | wrmo 2303 |
Extend wff notation to include restricted "at most one."
|
wff ∃*x ∈ A φ |
|
Syntax | crab 2304 |
Extend class notation to include the restricted class abstraction (class
builder).
|
class {x ∈ A ∣
φ} |
|
Definition | df-ral 2305 |
Define restricted universal quantification. Special case of Definition
4.15(3) of [TakeutiZaring] p. 22.
(Contributed by NM, 19-Aug-1993.)
|
⊢ (∀x ∈ A φ ↔
∀x(x ∈ A →
φ)) |
|
Definition | df-rex 2306 |
Define restricted existential quantification. Special case of Definition
4.15(4) of [TakeutiZaring] p. 22.
(Contributed by NM, 30-Aug-1993.)
|
⊢ (∃x ∈ A φ ↔
∃x(x ∈ A ∧ φ)) |
|
Definition | df-reu 2307 |
Define restricted existential uniqueness. (Contributed by NM,
22-Nov-1994.)
|
⊢ (∃!x ∈ A φ ↔
∃!x(x ∈ A ∧ φ)) |
|
Definition | df-rmo 2308 |
Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
|
⊢ (∃*x ∈ A φ ↔
∃*x(x ∈ A ∧ φ)) |
|
Definition | df-rab 2309 |
Define a restricted class abstraction (class builder), which is the class
of all x in
A such that φ is true.
Definition of
[TakeutiZaring] p. 20. (Contributed
by NM, 22-Nov-1994.)
|
⊢ {x ∈ A ∣
φ} = {x ∣ (x
∈ A
∧ φ)} |
|
Theorem | ralnex 2310 |
Relationship between restricted universal and existential quantifiers.
(Contributed by NM, 21-Jan-1997.)
|
⊢ (∀x ∈ A ¬ φ
↔ ¬ ∃x ∈ A φ) |
|
Theorem | rexnalim 2311 |
Relationship between restricted universal and existential quantifiers. In
classical logic this would be a biconditional. (Contributed by Jim
Kingdon, 17-Aug-2018.)
|
⊢ (∃x ∈ A ¬ φ
→ ¬ ∀x ∈ A φ) |
|
Theorem | ralexim 2312 |
Relationship between restricted universal and existential quantifiers.
(Contributed by Jim Kingdon, 17-Aug-2018.)
|
⊢ (∀x ∈ A φ →
¬ ∃x ∈ A ¬ φ) |
|
Theorem | rexalim 2313 |
Relationship between restricted universal and existential quantifiers.
(Contributed by Jim Kingdon, 17-Aug-2018.)
|
⊢ (∃x ∈ A φ →
¬ ∀x ∈ A ¬ φ) |
|
Theorem | ralbida 2314 |
Formula-building rule for restricted universal quantifier (deduction
rule). (Contributed by NM, 6-Oct-2003.)
|
⊢ Ⅎxφ
& ⊢ ((φ
∧ x ∈ A) →
(ψ ↔ χ)) ⇒ ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ)) |
|
Theorem | rexbida 2315 |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 6-Oct-2003.)
|
⊢ Ⅎxφ
& ⊢ ((φ
∧ x ∈ A) →
(ψ ↔ χ)) ⇒ ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ)) |
|
Theorem | ralbidva 2316* |
Formula-building rule for restricted universal quantifier (deduction
rule). (Contributed by NM, 4-Mar-1997.)
|
⊢ ((φ
∧ x ∈ A) →
(ψ ↔ χ)) ⇒ ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ)) |
|
Theorem | rexbidva 2317* |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 9-Mar-1997.)
|
⊢ ((φ
∧ x ∈ A) →
(ψ ↔ χ)) ⇒ ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ)) |
|
Theorem | ralbid 2318 |
Formula-building rule for restricted universal quantifier (deduction
rule). (Contributed by NM, 27-Jun-1998.)
|
⊢ Ⅎxφ
& ⊢ (φ
→ (ψ ↔ χ)) ⇒ ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ)) |
|
Theorem | rexbid 2319 |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 27-Jun-1998.)
|
⊢ Ⅎxφ
& ⊢ (φ
→ (ψ ↔ χ)) ⇒ ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ)) |
|
Theorem | ralbidv 2320* |
Formula-building rule for restricted universal quantifier (deduction
rule). (Contributed by NM, 20-Nov-1994.)
|
⊢ (φ
→ (ψ ↔ χ)) ⇒ ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ)) |
|
Theorem | rexbidv 2321* |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 20-Nov-1994.)
|
⊢ (φ
→ (ψ ↔ χ)) ⇒ ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ)) |
|
Theorem | ralbidv2 2322* |
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 2323* |
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 2324 |
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 2325 |
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 2326 |
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 2327 |
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 2328 |
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 2329 |
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 2330 |
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 2331 |
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 2332 |
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 2333 |
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 2334* |
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 2335* |
Double restricted universal quantification. (Contributed by Mario
Carneiro, 14-Oct-2016.)
|
⊢ ℲyA ⇒ ⊢ (∀x ∈ A ∀y ∈ B φ ↔ ∀x∀y((x ∈ A ∧ y ∈ B) → φ)) |
|
Theorem | r2exf 2336* |
Double restricted existential quantification. (Contributed by Mario
Carneiro, 14-Oct-2016.)
|
⊢ ℲyA ⇒ ⊢ (∃x ∈ A ∃y ∈ B φ ↔ ∃x∃y((x ∈ A ∧ y ∈ B) ∧ φ)) |
|
Theorem | r2al 2337* |
Double restricted universal quantification. (Contributed by NM,
19-Nov-1995.)
|
⊢ (∀x ∈ A ∀y ∈ B φ ↔
∀x∀y((x ∈ A ∧ y ∈ B) →
φ)) |
|
Theorem | r2ex 2338* |
Double restricted existential quantification. (Contributed by NM,
11-Nov-1995.)
|
⊢ (∃x ∈ A ∃y ∈ B φ ↔
∃x∃y((x ∈ A ∧ y ∈ B) ∧ φ)) |
|
Theorem | 2ralbida 2339* |
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 2340* |
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 2341* |
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 2342* |
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 2343* |
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 2344* |
Formula-building rule for restricted quantifiers (deduction rule).
(Contributed by NM, 28-Jan-2006.)
|
⊢ (φ
→ (ψ ↔ χ)) ⇒ ⊢ (φ → (∃x ∈ A ∀y ∈ B ψ ↔ ∃x ∈ A ∀y ∈ B χ)) |
|
Theorem | ralinexa 2345 |
A transformation of restricted quantifiers and logical connectives.
(Contributed by NM, 4-Sep-2005.)
|
⊢ (∀x ∈ A (φ →
¬ ψ) ↔ ¬ ∃x ∈ A (φ ∧ ψ)) |
|
Theorem | risset 2346* |
Two ways to say "A belongs to B." (Contributed by NM,
22-Nov-1994.)
|
⊢ (A ∈ B ↔
∃x
∈ B
x = A) |
|
Theorem | hbral 2347 |
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 2348 |
x is not free in
∀x ∈ Aφ.
(Contributed by NM,
18-Oct-1996.)
|
⊢ (∀x ∈ A φ →
∀x∀x ∈ A φ) |
|
Theorem | nfra1 2349 |
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 2350* |
Not-free for restricted universal quantification where x and y
are distinct. See nfraldya 2352 for a version with y and A
distinct instead. (Contributed by Jim Kingdon, 29-May-2018.)
|
⊢ Ⅎyφ
& ⊢ (φ
→ ℲxA)
& ⊢ (φ
→ Ⅎxψ) ⇒ ⊢ (φ → Ⅎx∀y ∈ A ψ) |
|
Theorem | nfrexdxy 2351* |
Not-free for restricted existential quantification where x and y
are distinct. See nfrexdya 2353 for a version with y and A
distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
|
⊢ Ⅎyφ
& ⊢ (φ
→ ℲxA)
& ⊢ (φ
→ Ⅎxψ) ⇒ ⊢ (φ → Ⅎx∃y ∈ A ψ) |
|
Theorem | nfraldya 2352* |
Not-free for restricted universal quantification where y and A
are distinct. See nfraldxy 2350 for a version with x and y
distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
|
⊢ Ⅎyφ
& ⊢ (φ
→ ℲxA)
& ⊢ (φ
→ Ⅎxψ) ⇒ ⊢ (φ → Ⅎx∀y ∈ A ψ) |
|
Theorem | nfrexdya 2353* |
Not-free for restricted existential quantification where y and A
are distinct. See nfrexdxy 2351 for a version with x and y
distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
|
⊢ Ⅎyφ
& ⊢ (φ
→ ℲxA)
& ⊢ (φ
→ Ⅎxψ) ⇒ ⊢ (φ → Ⅎx∃y ∈ A ψ) |
|
Theorem | nfralxy 2354* |
Not-free for restricted universal quantification where x and y
are distinct. See nfralya 2356 for a version with y and A distinct
instead. (Contributed by Jim Kingdon, 30-May-2018.)
|
⊢ ℲxA & ⊢
Ⅎxφ ⇒ ⊢ Ⅎx∀y ∈ A φ |
|
Theorem | nfrexxy 2355* |
Not-free for restricted existential quantification where x and y
are distinct. See nfrexya 2357 for a version with y and A distinct
instead. (Contributed by Jim Kingdon, 30-May-2018.)
|
⊢ ℲxA & ⊢
Ⅎxφ ⇒ ⊢ Ⅎx∃y ∈ A φ |
|
Theorem | nfralya 2356* |
Not-free for restricted universal quantification where y and A
are distinct. See nfralxy 2354 for a version with x and y distinct
instead. (Contributed by Jim Kingdon, 3-Jun-2018.)
|
⊢ ℲxA & ⊢
Ⅎxφ ⇒ ⊢ Ⅎx∀y ∈ A φ |
|
Theorem | nfrexya 2357* |
Not-free for restricted existential quantification where y and A
are distinct. See nfrexxy 2355 for a version with x and y distinct
instead. (Contributed by Jim Kingdon, 3-Jun-2018.)
|
⊢ ℲxA & ⊢
Ⅎxφ ⇒ ⊢ Ⅎx∃y ∈ A φ |
|
Theorem | nfra2xy 2358* |
Not-free given two restricted quantifiers. (Contributed by Jim Kingdon,
20-Aug-2018.)
|
⊢ Ⅎy∀x ∈ A ∀y ∈ B φ |
|
Theorem | nfre1 2359 |
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 2360* |
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 2361 |
Universal quantification implies restricted quantification. (Contributed
by NM, 20-Oct-2006.)
|
⊢ (∀xφ →
∀x
∈ A
φ) |
|
Theorem | rexex 2362 |
Restricted existence implies existence. (Contributed by NM,
11-Nov-1995.)
|
⊢ (∃x ∈ A φ →
∃xφ) |
|
Theorem | rsp 2363 |
Restricted specialization. (Contributed by NM, 17-Oct-1996.)
|
⊢ (∀x ∈ A φ →
(x ∈
A → φ)) |
|
Theorem | rspe 2364 |
Restricted specialization. (Contributed by NM, 12-Oct-1999.)
|
⊢ ((x ∈ A ∧ φ) →
∃x
∈ A
φ) |
|
Theorem | rsp2 2365 |
Restricted specialization. (Contributed by NM, 11-Feb-1997.)
|
⊢ (∀x ∈ A ∀y ∈ B φ →
((x ∈
A ∧
y ∈
B) → φ)) |
|
Theorem | rsp2e 2366 |
Restricted specialization. (Contributed by FL, 4-Jun-2012.)
|
⊢ ((x ∈ A ∧ y ∈ B ∧ φ) →
∃x
∈ A
∃y
∈ B
φ) |
|
Theorem | rspec 2367 |
Specialization rule for restricted quantification. (Contributed by NM,
19-Nov-1994.)
|
⊢ ∀x ∈ A φ ⇒ ⊢ (x ∈ A → φ) |
|
Theorem | rgen 2368 |
Generalization rule for restricted quantification. (Contributed by NM,
19-Nov-1994.)
|
⊢ (x ∈ A →
φ) ⇒ ⊢ ∀x ∈ A φ |
|
Theorem | rgen2a 2369* |
Generalization rule for restricted quantification. Note that x and
y needn't be
distinct (and illustrates the use of dvelimor 1891).
(Contributed by NM, 23-Nov-1994.) (Proof rewritten by Jim Kingdon,
1-Jun-2018.)
|
⊢ ((x ∈ A ∧ y ∈ A) →
φ) ⇒ ⊢ ∀x ∈ A ∀y ∈ A φ |
|
Theorem | rgenw 2370 |
Generalization rule for restricted quantification. (Contributed by NM,
18-Jun-2014.)
|
⊢ φ ⇒ ⊢ ∀x ∈ A φ |
|
Theorem | rgen2w 2371 |
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 2372 |
Modus ponens combined with restricted generalization. (Contributed by
NM, 10-Aug-2004.)
|
⊢ (∀x ∈ A φ →
ψ) & ⊢ (x ∈ A → φ) ⇒ ⊢ ψ |
|
Theorem | mprgbir 2373 |
Modus ponens on biconditional combined with restricted generalization.
(Contributed by NM, 21-Mar-2004.)
|
⊢ (φ
↔ ∀x ∈ A ψ)
& ⊢ (x ∈ A →
ψ) ⇒ ⊢ φ |
|
Theorem | ralim 2374 |
Distribution of restricted quantification over implication. (Contributed
by NM, 9-Feb-1997.)
|
⊢ (∀x ∈ A (φ →
ψ) → (∀x ∈ A φ → ∀x ∈ A ψ)) |
|
Theorem | ralimi2 2375 |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 22-Feb-2004.)
|
⊢ ((x ∈ A →
φ) → (x ∈ B → ψ)) ⇒ ⊢ (∀x ∈ A φ → ∀x ∈ B ψ) |
|
Theorem | ralimia 2376 |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 19-Jul-1996.)
|
⊢ (x ∈ A →
(φ → ψ)) ⇒ ⊢ (∀x ∈ A φ → ∀x ∈ A ψ) |
|
Theorem | ralimiaa 2377 |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 4-Aug-2007.)
|
⊢ ((x ∈ A ∧ φ) →
ψ) ⇒ ⊢ (∀x ∈ A φ → ∀x ∈ A ψ) |
|
Theorem | ralimi 2378 |
Inference quantifying both antecedent and consequent, with strong
hypothesis. (Contributed by NM, 4-Mar-1997.)
|
⊢ (φ
→ ψ)
⇒ ⊢ (∀x ∈ A φ → ∀x ∈ A ψ) |
|
Theorem | ral2imi 2379 |
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 2380 |
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 2381* |
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 2382* |
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 2383* |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 1-Feb-2005.)
|
⊢ (φ
→ ((x ∈ A →
ψ) → (x ∈ B → χ))) ⇒ ⊢ (φ → (∀x ∈ A ψ → ∀x ∈ B χ)) |
|
Theorem | ralrimi 2384 |
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 2385* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 22-Nov-1994.)
|
⊢ (φ
→ (x ∈ A →
ψ)) ⇒ ⊢ (φ → ∀x ∈ A ψ) |
|
Theorem | ralrimiva 2386* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 2-Jan-2006.)
|
⊢ ((φ
∧ x ∈ A) →
ψ) ⇒ ⊢ (φ → ∀x ∈ A ψ) |
|
Theorem | ralrimivw 2387* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 18-Jun-2014.)
|
⊢ (φ
→ ψ)
⇒ ⊢ (φ → ∀x ∈ A ψ) |
|
Theorem | r19.21t 2388 |
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 2389 |
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 2390* |
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 2391 |
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 2392* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 27-May-1998.)
|
⊢ (φ
→ (ψ → (x ∈ A → χ))) ⇒ ⊢ (φ → (ψ → ∀x ∈ A χ)) |
|
Theorem | ralrimdva 2393* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 2-Feb-2008.)
|
⊢ ((φ
∧ x ∈ A) →
(ψ → χ)) ⇒ ⊢ (φ → (ψ → ∀x ∈ A χ)) |
|
Theorem | ralrimivv 2394* |
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 2395* |
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 2396* |
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 2397* |
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 2398* |
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 2399* |
Generalization rule for restricted quantification. (Contributed by NM,
30-May-1999.)
|
⊢ ((x ∈ A ∧ y ∈ B) →
φ) ⇒ ⊢ ∀x ∈ A ∀y ∈ B φ |
|
Theorem | rgen3 2400* |
Generalization rule for restricted quantification. (Contributed by NM,
12-Jan-2008.)
|
⊢ ((x ∈ A ∧ y ∈ B ∧ z ∈ 𝐶) → φ) ⇒ ⊢ ∀x ∈ A ∀y ∈ B ∀z ∈ 𝐶 φ |