Theorem List for Intuitionistic Logic Explorer - 2601-2700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | r19.29 2601 |
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 2602 |
Variation of Theorem 19.29 of [Margaris] p. 90
with restricted
quantifiers. (Contributed by NM, 31-Aug-1999.)
|
|
|
Theorem | ralnex2 2603 |
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 2604 |
A commonly used pattern based on r19.29 2601. (Contributed by Thierry
Arnoux, 17-Dec-2017.)
|
|
|
Theorem | r19.29af 2605* |
A commonly used pattern based on r19.29 2601. (Contributed by Thierry
Arnoux, 29-Nov-2017.)
|
|
|
Theorem | r19.29an 2606* |
A commonly used pattern based on r19.29 2601. (Contributed by Thierry
Arnoux, 29-Dec-2019.)
|
|
|
Theorem | r19.29a 2607* |
A commonly used pattern based on r19.29 2601. (Contributed by Thierry
Arnoux, 22-Nov-2017.)
|
|
|
Theorem | r19.29d2r 2608 |
Theorem 19.29 of [Margaris] p. 90 with two
restricted quantifiers,
deduction version. (Contributed by Thierry Arnoux, 30-Jan-2017.)
|
|
|
Theorem | r19.29vva 2609* |
A commonly used pattern based on r19.29 2601, version with two restricted
quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.)
|
|
|
Theorem | r19.32r 2610 |
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.30dc 2611 |
Restricted quantifier version of 19.30dc 1614. (Contributed by Scott
Fenton, 25-Feb-2011.) (Proof shortened by Wolf Lammen, 18-Jun-2023.)
|
DECID
|
|
Theorem | r19.32vr 2612* |
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 2613. (Contributed by Jim Kingdon, 19-Aug-2018.)
|
|
|
Theorem | r19.32vdc 2613* |
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 2614 |
Restricted quantifier version of 19.35-1 1611. (Contributed by Jim Kingdon,
4-Jun-2018.)
|
|
|
Theorem | r19.36av 2615* |
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 2616 |
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 2617* |
Restricted version of one direction of Theorem 19.37 of [Margaris]
p. 90. (Contributed by NM, 2-Apr-2004.)
|
|
|
Theorem | r19.40 2618 |
Restricted quantifier version of Theorem 19.40 of [Margaris] p. 90.
(Contributed by NM, 2-Apr-2004.)
|
|
|
Theorem | r19.41 2619 |
Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
(Contributed by NM, 1-Nov-2010.)
|
|
|
Theorem | r19.41v 2620* |
Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
(Contributed by NM, 17-Dec-2003.)
|
|
|
Theorem | r19.42v 2621* |
Restricted version of Theorem 19.42 of [Margaris] p. 90. (Contributed
by NM, 27-May-1998.)
|
|
|
Theorem | r19.43 2622 |
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 2623* |
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 2624* |
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 2625* |
Commutation of restricted quantifiers. (Contributed by Mario Carneiro,
14-Oct-2016.)
|
|
|
Theorem | rexcomf 2626* |
Commutation of restricted quantifiers. (Contributed by Mario Carneiro,
14-Oct-2016.)
|
|
|
Theorem | ralcom 2627* |
Commutation of restricted quantifiers. (Contributed by NM,
13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
|
|
Theorem | rexcom 2628* |
Commutation of restricted quantifiers. (Contributed by NM,
19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
|
|
Theorem | rexcom13 2629* |
Swap 1st and 3rd restricted existential quantifiers. (Contributed by
NM, 8-Apr-2015.)
|
|
|
Theorem | rexrot4 2630* |
Rotate existential restricted quantifiers twice. (Contributed by NM,
8-Apr-2015.)
|
|
|
Theorem | ralcom3 2631 |
A commutative law for restricted quantifiers that swaps the domain of the
restriction. (Contributed by NM, 22-Feb-2004.)
|
|
|
Theorem | reean 2632* |
Rearrange existential quantifiers. (Contributed by NM, 27-Oct-2010.)
(Proof shortened by Andrew Salmon, 30-May-2011.)
|
|
|
Theorem | reeanv 2633* |
Rearrange existential quantifiers. (Contributed by NM, 9-May-1999.)
|
|
|
Theorem | 3reeanv 2634* |
Rearrange three existential quantifiers. (Contributed by Jeff Madsen,
11-Jun-2010.)
|
|
|
Theorem | nfreu1 2635 |
is not free in .
(Contributed by NM,
19-Mar-1997.)
|
|
|
Theorem | nfrmo1 2636 |
is not free in .
(Contributed by NM,
16-Jun-2017.)
|
|
|
Theorem | nfreudxy 2637* |
Not-free deduction for restricted uniqueness. This is a version where
and are distinct. (Contributed
by Jim Kingdon,
6-Jun-2018.)
|
|
|
Theorem | nfreuxy 2638* |
Not-free for restricted uniqueness. This is a version where and
are distinct.
(Contributed by Jim Kingdon, 6-Jun-2018.)
|
|
|
Theorem | rabid 2639 |
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 2640* |
An "identity" law for restricted class abstraction. (Contributed by
NM,
9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|
|
|
Theorem | rabbi 2641 |
Equivalent wff's correspond to equal restricted class abstractions.
Closed theorem form of rabbidva 2709. (Contributed by NM, 25-Nov-2013.)
|
|
|
Theorem | rabswap 2642 |
Swap with a membership relation in a restricted class abstraction.
(Contributed by NM, 4-Jul-2005.)
|
|
|
Theorem | nfrab1 2643 |
The abstraction variable in a restricted class abstraction isn't free.
(Contributed by NM, 19-Mar-1997.)
|
|
|
Theorem | nfrabxy 2644* |
A variable not free in a wff remains so in a restricted class
abstraction. (Contributed by Jim Kingdon, 19-Jul-2018.)
|
|
|
Theorem | reubida 2645 |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by Mario Carneiro, 19-Nov-2016.)
|
|
|
Theorem | reubidva 2646* |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 13-Nov-2004.)
|
|
|
Theorem | reubidv 2647* |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 17-Oct-1996.)
|
|
|
Theorem | reubiia 2648 |
Formula-building rule for restricted existential quantifier (inference
form). (Contributed by NM, 14-Nov-2004.)
|
|
|
Theorem | reubii 2649 |
Formula-building rule for restricted existential quantifier (inference
form). (Contributed by NM, 22-Oct-1999.)
|
|
|
Theorem | rmobida 2650 |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 16-Jun-2017.)
|
|
|
Theorem | rmobidva 2651* |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 16-Jun-2017.)
|
|
|
Theorem | rmobidv 2652* |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 16-Jun-2017.)
|
|
|
Theorem | rmobiia 2653 |
Formula-building rule for restricted existential quantifier (inference
form). (Contributed by NM, 16-Jun-2017.)
|
|
|
Theorem | rmobii 2654 |
Formula-building rule for restricted existential quantifier (inference
form). (Contributed by NM, 16-Jun-2017.)
|
|
|
Theorem | raleqf 2655 |
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 2656 |
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 2657 |
Equality theorem for restricted unique existential 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 2658 |
Equality theorem for restricted at-most-one quantifier, with
bound-variable hypotheses instead of distinct variable restrictions.
(Contributed by Alexander van der Vekens, 17-Jun-2017.)
|
|
|
Theorem | raleq 2659* |
Equality theorem for restricted universal quantifier. (Contributed by
NM, 16-Nov-1995.)
|
|
|
Theorem | rexeq 2660* |
Equality theorem for restricted existential quantifier. (Contributed by
NM, 29-Oct-1995.)
|
|
|
Theorem | reueq1 2661* |
Equality theorem for restricted unique existential quantifier.
(Contributed by NM, 5-Apr-2004.)
|
|
|
Theorem | rmoeq1 2662* |
Equality theorem for restricted at-most-one quantifier. (Contributed by
Alexander van der Vekens, 17-Jun-2017.)
|
|
|
Theorem | raleqi 2663* |
Equality inference for restricted universal qualifier. (Contributed by
Paul Chapman, 22-Jun-2011.)
|
|
|
Theorem | rexeqi 2664* |
Equality inference for restricted existential qualifier. (Contributed
by Mario Carneiro, 23-Apr-2015.)
|
|
|
Theorem | raleqdv 2665* |
Equality deduction for restricted universal quantifier. (Contributed by
NM, 13-Nov-2005.)
|
|
|
Theorem | rexeqdv 2666* |
Equality deduction for restricted existential quantifier. (Contributed
by NM, 14-Jan-2007.)
|
|
|
Theorem | raleqbi1dv 2667* |
Equality deduction for restricted universal quantifier. (Contributed by
NM, 16-Nov-1995.)
|
|
|
Theorem | rexeqbi1dv 2668* |
Equality deduction for restricted existential quantifier. (Contributed
by NM, 18-Mar-1997.)
|
|
|
Theorem | reueqd 2669* |
Equality deduction for restricted unique existential quantifier.
(Contributed by NM, 5-Apr-2004.)
|
|
|
Theorem | rmoeqd 2670* |
Equality deduction for restricted at-most-one quantifier. (Contributed
by Alexander van der Vekens, 17-Jun-2017.)
|
|
|
Theorem | raleqbidv 2671* |
Equality deduction for restricted universal quantifier. (Contributed by
NM, 6-Nov-2007.)
|
|
|
Theorem | rexeqbidv 2672* |
Equality deduction for restricted universal quantifier. (Contributed by
NM, 6-Nov-2007.)
|
|
|
Theorem | raleqbidva 2673* |
Equality deduction for restricted universal quantifier. (Contributed by
Mario Carneiro, 5-Jan-2017.)
|
|
|
Theorem | rexeqbidva 2674* |
Equality deduction for restricted universal quantifier. (Contributed by
Mario Carneiro, 5-Jan-2017.)
|
|
|
Theorem | mormo 2675 |
Unrestricted "at most one" implies restricted "at most
one". (Contributed
by NM, 16-Jun-2017.)
|
|
|
Theorem | reu5 2676 |
Restricted uniqueness in terms of "at most one." (Contributed by NM,
23-May-1999.) (Revised by NM, 16-Jun-2017.)
|
|
|
Theorem | reurex 2677 |
Restricted unique existence implies restricted existence. (Contributed by
NM, 19-Aug-1999.)
|
|
|
Theorem | reurmo 2678 |
Restricted existential uniqueness implies restricted "at most one."
(Contributed by NM, 16-Jun-2017.)
|
|
|
Theorem | rmo5 2679 |
Restricted "at most one" in term of uniqueness. (Contributed by NM,
16-Jun-2017.)
|
|
|
Theorem | nrexrmo 2680 |
Nonexistence implies restricted "at most one". (Contributed by NM,
17-Jun-2017.)
|
|
|
Theorem | cbvralfw 2681* |
Rule used to change bound variables, using implicit substitution.
Version of cbvralf 2682 with a disjoint variable condition. Although
we
don't do so yet, we expect this disjoint variable condition will allow
us to remove reliance on ax-i12 1494 and ax-bndl 1496 in the proof.
(Contributed by NM, 7-Mar-2004.) (Revised by Gino Giotto,
23-May-2024.)
|
|
|
Theorem | cbvralf 2682 |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 7-Mar-2004.) (Revised by Mario Carneiro,
9-Oct-2016.)
|
|
|
Theorem | cbvrexf 2683 |
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 | cbvralw 2684* |
Rule used to change bound variables, using implicit substitution.
Version of cbvral 2685 with a disjoint variable condition. Although
we
don't do so yet, we expect this disjoint variable condition will allow
us to remove reliance on ax-i12 1494 and ax-bndl 1496 in the proof.
(Contributed by NM, 31-Jul-2003.) (Revised by Gino Giotto,
10-Jan-2024.)
|
|
|
Theorem | cbvral 2685* |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 31-Jul-2003.)
|
|
|
Theorem | cbvrex 2686* |
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 2687* |
Change the bound variable of a restricted unique existential quantifier
using implicit substitution. (Contributed by Mario Carneiro,
15-Oct-2016.)
|
|
|
Theorem | cbvrmo 2688* |
Change the bound variable of restricted "at most one" using implicit
substitution. (Contributed by NM, 16-Jun-2017.)
|
|
|
Theorem | cbvralv 2689* |
Change the bound variable of a restricted universal quantifier using
implicit substitution. (Contributed by NM, 28-Jan-1997.)
|
|
|
Theorem | cbvrexv 2690* |
Change the bound variable of a restricted existential quantifier using
implicit substitution. (Contributed by NM, 2-Jun-1998.)
|
|
|
Theorem | cbvreuv 2691* |
Change the bound variable of a restricted unique existential quantifier
using implicit substitution. (Contributed by NM, 5-Apr-2004.) (Revised
by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | cbvrmov 2692* |
Change the bound variable of a restricted at-most-one quantifier using
implicit substitution. (Contributed by Alexander van der Vekens,
17-Jun-2017.)
|
|
|
Theorem | cbvralvw 2693* |
Version of cbvralv 2689 with a disjoint variable condition.
(Contributed
by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino
Giotto, 25-Aug-2024.)
|
|
|
Theorem | cbvrexvw 2694* |
Version of cbvrexv 2690 with a disjoint variable condition.
(Contributed
by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino
Giotto, 25-Aug-2024.)
|
|
|
Theorem | cbvreuvw 2695* |
Version of cbvreuv 2691 with a disjoint variable condition.
(Contributed
by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino
Giotto, 25-Aug-2024.)
|
|
|
Theorem | cbvraldva2 2696* |
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 2697* |
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 2698* |
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 2699* |
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 2700* |
Change bound variables of double restricted universal quantification,
using implicit substitution. (Contributed by NM, 10-Aug-2004.)
|
|