Theorem List for Intuitionistic Logic Explorer - 2501-2600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | r19.32r 2501 |
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 2502* |
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 2503. (Contributed by Jim Kingdon, 19-Aug-2018.)
|
|
|
Theorem | r19.32vdc 2503* |
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 2504 |
Restricted quantifier version of 19.35-1 1555. (Contributed by Jim Kingdon,
4-Jun-2018.)
|
|
|
Theorem | r19.36av 2505* |
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 2506 |
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 2507* |
Restricted version of one direction of Theorem 19.37 of [Margaris]
p. 90. (Contributed by NM, 2-Apr-2004.)
|
|
|
Theorem | r19.40 2508 |
Restricted quantifier version of Theorem 19.40 of [Margaris] p. 90.
(Contributed by NM, 2-Apr-2004.)
|
|
|
Theorem | r19.41 2509 |
Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
(Contributed by NM, 1-Nov-2010.)
|
|
|
Theorem | r19.41v 2510* |
Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
(Contributed by NM, 17-Dec-2003.)
|
|
|
Theorem | r19.42v 2511* |
Restricted version of Theorem 19.42 of [Margaris] p. 90. (Contributed
by NM, 27-May-1998.)
|
|
|
Theorem | r19.43 2512 |
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 2513* |
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 2514* |
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 2515* |
Commutation of restricted quantifiers. (Contributed by Mario Carneiro,
14-Oct-2016.)
|
|
|
Theorem | rexcomf 2516* |
Commutation of restricted quantifiers. (Contributed by Mario Carneiro,
14-Oct-2016.)
|
|
|
Theorem | ralcom 2517* |
Commutation of restricted quantifiers. (Contributed by NM,
13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
|
|
Theorem | rexcom 2518* |
Commutation of restricted quantifiers. (Contributed by NM,
19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
|
|
Theorem | rexcom13 2519* |
Swap 1st and 3rd restricted existential quantifiers. (Contributed by
NM, 8-Apr-2015.)
|
|
|
Theorem | rexrot4 2520* |
Rotate existential restricted quantifiers twice. (Contributed by NM,
8-Apr-2015.)
|
|
|
Theorem | ralcom3 2521 |
A commutative law for restricted quantifiers that swaps the domain of the
restriction. (Contributed by NM, 22-Feb-2004.)
|
|
|
Theorem | reean 2522* |
Rearrange existential quantifiers. (Contributed by NM, 27-Oct-2010.)
(Proof shortened by Andrew Salmon, 30-May-2011.)
|
|
|
Theorem | reeanv 2523* |
Rearrange existential quantifiers. (Contributed by NM, 9-May-1999.)
|
|
|
Theorem | 3reeanv 2524* |
Rearrange three existential quantifiers. (Contributed by Jeff Madsen,
11-Jun-2010.)
|
|
|
Theorem | nfreu1 2525 |
is not free in .
(Contributed by NM,
19-Mar-1997.)
|
|
|
Theorem | nfrmo1 2526 |
is not free in .
(Contributed by NM,
16-Jun-2017.)
|
|
|
Theorem | nfreudxy 2527* |
Not-free deduction for restricted uniqueness. This is a version where
and are distinct. (Contributed
by Jim Kingdon,
6-Jun-2018.)
|
|
|
Theorem | nfreuxy 2528* |
Not-free for restricted uniqueness. This is a version where and
are distinct.
(Contributed by Jim Kingdon, 6-Jun-2018.)
|
|
|
Theorem | rabid 2529 |
An "identity" law of concretion for restricted abstraction. Special
case
of Definition 2.1 of [Quine] p. 16.
(Contributed by NM, 9-Oct-2003.)
|
|
|
Theorem | rabid2 2530* |
An "identity" law for restricted class abstraction. (Contributed by
NM,
9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|
|
|
Theorem | rabbi 2531 |
Equivalent wff's correspond to equal restricted class abstractions.
Closed theorem form of rabbidva 2592. (Contributed by NM, 25-Nov-2013.)
|
|
|
Theorem | rabswap 2532 |
Swap with a membership relation in a restricted class abstraction.
(Contributed by NM, 4-Jul-2005.)
|
|
|
Theorem | nfrab1 2533 |
The abstraction variable in a restricted class abstraction isn't free.
(Contributed by NM, 19-Mar-1997.)
|
|
|
Theorem | nfrabxy 2534* |
A variable not free in a wff remains so in a restricted class
abstraction. (Contributed by Jim Kingdon, 19-Jul-2018.)
|
|
|
Theorem | reubida 2535 |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by Mario Carneiro, 19-Nov-2016.)
|
|
|
Theorem | reubidva 2536* |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 13-Nov-2004.)
|
|
|
Theorem | reubidv 2537* |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 17-Oct-1996.)
|
|
|
Theorem | reubiia 2538 |
Formula-building rule for restricted existential quantifier (inference
rule). (Contributed by NM, 14-Nov-2004.)
|
|
|
Theorem | reubii 2539 |
Formula-building rule for restricted existential quantifier (inference
rule). (Contributed by NM, 22-Oct-1999.)
|
|
|
Theorem | rmobida 2540 |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 16-Jun-2017.)
|
|
|
Theorem | rmobidva 2541* |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 16-Jun-2017.)
|
|
|
Theorem | rmobidv 2542* |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 16-Jun-2017.)
|
|
|
Theorem | rmobiia 2543 |
Formula-building rule for restricted existential quantifier (inference
rule). (Contributed by NM, 16-Jun-2017.)
|
|
|
Theorem | rmobii 2544 |
Formula-building rule for restricted existential quantifier (inference
rule). (Contributed by NM, 16-Jun-2017.)
|
|
|
Theorem | raleqf 2545 |
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.)
|
|
|
Theorem | rexeqf 2546 |
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.)
|
|
|
Theorem | reueq1f 2547 |
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.)
|
|
|
Theorem | rmoeq1f 2548 |
Equality theorem for restricted uniqueness quantifier, with
bound-variable hypotheses instead of distinct variable restrictions.
(Contributed by Alexander van der Vekens, 17-Jun-2017.)
|
|
|
Theorem | raleq 2549* |
Equality theorem for restricted universal quantifier. (Contributed by
NM, 16-Nov-1995.)
|
|
|
Theorem | rexeq 2550* |
Equality theorem for restricted existential quantifier. (Contributed by
NM, 29-Oct-1995.)
|
|
|
Theorem | reueq1 2551* |
Equality theorem for restricted uniqueness quantifier. (Contributed by
NM, 5-Apr-2004.)
|
|
|
Theorem | rmoeq1 2552* |
Equality theorem for restricted uniqueness quantifier. (Contributed by
Alexander van der Vekens, 17-Jun-2017.)
|
|
|
Theorem | raleqi 2553* |
Equality inference for restricted universal qualifier. (Contributed by
Paul Chapman, 22-Jun-2011.)
|
|
|
Theorem | rexeqi 2554* |
Equality inference for restricted existential qualifier. (Contributed
by Mario Carneiro, 23-Apr-2015.)
|
|
|
Theorem | raleqdv 2555* |
Equality deduction for restricted universal quantifier. (Contributed by
NM, 13-Nov-2005.)
|
|
|
Theorem | rexeqdv 2556* |
Equality deduction for restricted existential quantifier. (Contributed
by NM, 14-Jan-2007.)
|
|
|
Theorem | raleqbi1dv 2557* |
Equality deduction for restricted universal quantifier. (Contributed by
NM, 16-Nov-1995.)
|
|
|
Theorem | rexeqbi1dv 2558* |
Equality deduction for restricted existential quantifier. (Contributed
by NM, 18-Mar-1997.)
|
|
|
Theorem | reueqd 2559* |
Equality deduction for restricted uniqueness quantifier. (Contributed
by NM, 5-Apr-2004.)
|
|
|
Theorem | rmoeqd 2560* |
Equality deduction for restricted uniqueness quantifier. (Contributed
by Alexander van der Vekens, 17-Jun-2017.)
|
|
|
Theorem | raleqbidv 2561* |
Equality deduction for restricted universal quantifier. (Contributed by
NM, 6-Nov-2007.)
|
|
|
Theorem | rexeqbidv 2562* |
Equality deduction for restricted universal quantifier. (Contributed by
NM, 6-Nov-2007.)
|
|
|
Theorem | raleqbidva 2563* |
Equality deduction for restricted universal quantifier. (Contributed by
Mario Carneiro, 5-Jan-2017.)
|
|
|
Theorem | rexeqbidva 2564* |
Equality deduction for restricted universal quantifier. (Contributed by
Mario Carneiro, 5-Jan-2017.)
|
|
|
Theorem | mormo 2565 |
Unrestricted "at most one" implies restricted "at most
one". (Contributed
by NM, 16-Jun-2017.)
|
|
|
Theorem | reu5 2566 |
Restricted uniqueness in terms of "at most one." (Contributed by NM,
23-May-1999.) (Revised by NM, 16-Jun-2017.)
|
|
|
Theorem | reurex 2567 |
Restricted unique existence implies restricted existence. (Contributed by
NM, 19-Aug-1999.)
|
|
|
Theorem | reurmo 2568 |
Restricted existential uniqueness implies restricted "at most one."
(Contributed by NM, 16-Jun-2017.)
|
|
|
Theorem | rmo5 2569 |
Restricted "at most one" in term of uniqueness. (Contributed by NM,
16-Jun-2017.)
|
|
|
Theorem | nrexrmo 2570 |
Nonexistence implies restricted "at most one". (Contributed by NM,
17-Jun-2017.)
|
|
|
Theorem | cbvralf 2571 |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 7-Mar-2004.) (Revised by Mario Carneiro,
9-Oct-2016.)
|
|
|
Theorem | cbvrexf 2572 |
Rule used to change bound variables, using implicit substitution.
(Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro,
9-Oct-2016.) (Proof rewritten by Jim Kingdon, 10-Jun-2018.)
|
|
|
Theorem | cbvral 2573* |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 31-Jul-2003.)
|
|
|
Theorem | cbvrex 2574* |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 31-Jul-2003.) (Proof shortened by Andrew Salmon,
8-Jun-2011.)
|
|
|
Theorem | cbvreu 2575* |
Change the bound variable of a restricted uniqueness quantifier using
implicit substitution. (Contributed by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | cbvrmo 2576* |
Change the bound variable of restricted "at most one" using implicit
substitution. (Contributed by NM, 16-Jun-2017.)
|
|
|
Theorem | cbvralv 2577* |
Change the bound variable of a restricted universal quantifier using
implicit substitution. (Contributed by NM, 28-Jan-1997.)
|
|
|
Theorem | cbvrexv 2578* |
Change the bound variable of a restricted existential quantifier using
implicit substitution. (Contributed by NM, 2-Jun-1998.)
|
|
|
Theorem | cbvreuv 2579* |
Change the bound variable of a restricted uniqueness quantifier using
implicit substitution. (Contributed by NM, 5-Apr-2004.) (Revised by
Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | cbvrmov 2580* |
Change the bound variable of a restricted uniqueness quantifier using
implicit substitution. (Contributed by Alexander van der Vekens,
17-Jun-2017.)
|
|
|
Theorem | cbvraldva2 2581* |
Rule used to change the bound variable in a restricted universal
quantifier with implicit substitution which also changes the quantifier
domain. Deduction form. (Contributed by David Moews, 1-May-2017.)
|
|
|
Theorem | cbvrexdva2 2582* |
Rule used to change the bound variable in a restricted existential
quantifier with implicit substitution which also changes the quantifier
domain. Deduction form. (Contributed by David Moews, 1-May-2017.)
|
|
|
Theorem | cbvraldva 2583* |
Rule used to change the bound variable in a restricted universal
quantifier with implicit substitution. Deduction form. (Contributed by
David Moews, 1-May-2017.)
|
|
|
Theorem | cbvrexdva 2584* |
Rule used to change the bound variable in a restricted existential
quantifier with implicit substitution. Deduction form. (Contributed by
David Moews, 1-May-2017.)
|
|
|
Theorem | cbvral2v 2585* |
Change bound variables of double restricted universal quantification,
using implicit substitution. (Contributed by NM, 10-Aug-2004.)
|
|
|
Theorem | cbvrex2v 2586* |
Change bound variables of double restricted universal quantification,
using implicit substitution. (Contributed by FL, 2-Jul-2012.)
|
|
|
Theorem | cbvral3v 2587* |
Change bound variables of triple restricted universal quantification,
using implicit substitution. (Contributed by NM, 10-May-2005.)
|
|
|
Theorem | cbvralsv 2588* |
Change bound variable by using a substitution. (Contributed by NM,
20-Nov-2005.) (Revised by Andrew Salmon, 11-Jul-2011.)
|
|
|
Theorem | cbvrexsv 2589* |
Change bound variable by using a substitution. (Contributed by NM,
2-Mar-2008.) (Revised by Andrew Salmon, 11-Jul-2011.)
|
|
|
Theorem | sbralie 2590* |
Implicit to explicit substitution that swaps variables in a quantified
expression. (Contributed by NM, 5-Sep-2004.)
|
|
|
Theorem | rabbiia 2591 |
Equivalent wff's yield equal restricted class abstractions (inference
rule). (Contributed by NM, 22-May-1999.)
|
|
|
Theorem | rabbidva 2592* |
Equivalent wff's yield equal restricted class abstractions (deduction
rule). (Contributed by NM, 28-Nov-2003.)
|
|
|
Theorem | rabbidv 2593* |
Equivalent wff's yield equal restricted class abstractions (deduction
rule). (Contributed by NM, 10-Feb-1995.)
|
|
|
Theorem | rabeqf 2594 |
Equality theorem for restricted class abstractions, with bound-variable
hypotheses instead of distinct variable restrictions. (Contributed by
NM, 7-Mar-2004.)
|
|
|
Theorem | rabeq 2595* |
Equality theorem for restricted class abstractions. (Contributed by NM,
15-Oct-2003.)
|
|
|
Theorem | rabeqbidv 2596* |
Equality of restricted class abstractions. (Contributed by Jeff Madsen,
1-Dec-2009.)
|
|
|
Theorem | rabeqbidva 2597* |
Equality of restricted class abstractions. (Contributed by Mario
Carneiro, 26-Jan-2017.)
|
|
|
Theorem | rabeq2i 2598 |
Inference rule from equality of a class variable and a restricted class
abstraction. (Contributed by NM, 16-Feb-2004.)
|
|
|
Theorem | cbvrab 2599 |
Rule to change the bound variable in a restricted class abstraction,
using implicit substitution. This version has bound-variable hypotheses
in place of distinct variable conditions. (Contributed by Andrew
Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 9-Oct-2016.)
|
|
|
Theorem | cbvrabv 2600* |
Rule to change the bound variable in a restricted class abstraction,
using implicit substitution. (Contributed by NM, 26-May-1999.)
|
|