Type  Label  Description 
Statement 

Theorem  r19.21bi 2401 
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 20Nov1994.)



Theorem  rspec2 2402 
Specialization rule for restricted quantification. (Contributed by NM,
20Nov1994.)



Theorem  rspec3 2403 
Specialization rule for restricted quantification. (Contributed by NM,
20Nov1994.)



Theorem  r19.21be 2404 
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 21Nov1994.)



Theorem  nrex 2405 
Inference adding restricted existential quantifier to negated wff.
(Contributed by NM, 16Oct2003.)



Theorem  nrexdv 2406* 
Deduction adding restricted existential quantifier to negated wff.
(Contributed by NM, 16Oct2003.)



Theorem  rexim 2407 
Theorem 19.22 of [Margaris] p. 90.
(Restricted quantifier version.)
(Contributed by NM, 22Nov1994.) (Proof shortened by Andrew Salmon,
30May2011.)



Theorem  reximia 2408 
Inference quantifying both antecedent and consequent. (Contributed by
NM, 10Feb1997.)



Theorem  reximi2 2409 
Inference quantifying both antecedent and consequent, based on Theorem
19.22 of [Margaris] p. 90.
(Contributed by NM, 8Nov2004.)



Theorem  reximi 2410 
Inference quantifying both antecedent and consequent. (Contributed by
NM, 18Oct1996.)



Theorem  reximdai 2411 
Deduction from Theorem 19.22 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 31Aug1999.)



Theorem  reximdv2 2412* 
Deduction quantifying both antecedent and consequent, based on Theorem
19.22 of [Margaris] p. 90.
(Contributed by NM, 17Sep2003.)



Theorem  reximdvai 2413* 
Deduction quantifying both antecedent and consequent, based on Theorem
19.22 of [Margaris] p. 90.
(Contributed by NM, 14Nov2002.)



Theorem  reximdv 2414* 
Deduction from Theorem 19.22 of [Margaris] p.
90. (Restricted
quantifier version with strong hypothesis.) (Contributed by NM,
24Jun1998.)



Theorem  reximdva 2415* 
Deduction quantifying both antecedent and consequent, based on Theorem
19.22 of [Margaris] p. 90.
(Contributed by NM, 22May1999.)



Theorem  r19.12 2416* 
Theorem 19.12 of [Margaris] p. 89 with
restricted quantifiers.
(Contributed by NM, 15Oct2003.) (Proof shortened by Andrew Salmon,
30May2011.)



Theorem  r19.23t 2417 
Closed theorem form of r19.23 2418. (Contributed by NM, 4Mar2013.)
(Revised by Mario Carneiro, 8Oct2016.)



Theorem  r19.23 2418 
Theorem 19.23 of [Margaris] p. 90 with
restricted quantifiers.
(Contributed by NM, 22Oct2010.) (Proof shortened by Mario Carneiro,
8Oct2016.)



Theorem  r19.23v 2419* 
Theorem 19.23 of [Margaris] p. 90 with
restricted quantifiers.
(Contributed by NM, 31Aug1999.)



Theorem  rexlimi 2420 
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 30Nov2003.) (Proof
shortened by Andrew Salmon, 30May2011.)



Theorem  rexlimiv 2421* 
Inference from Theorem 19.23 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 20Nov1994.)



Theorem  rexlimiva 2422* 
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 18Dec2006.)



Theorem  rexlimivw 2423* 
Weaker version of rexlimiv 2421. (Contributed by FL, 19Sep2011.)



Theorem  rexlimd 2424 
Deduction from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 27May1998.) (Proof shortened by Andrew
Salmon, 30May2011.)



Theorem  rexlimd2 2425 
Version of rexlimd 2424 with deduction version of second hypothesis.
(Contributed by NM, 21Jul2013.) (Revised by Mario Carneiro,
8Oct2016.)



Theorem  rexlimdv 2426* 
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 14Nov2002.) (Proof shortened by Eric
Schmidt, 22Dec2006.)



Theorem  rexlimdva 2427* 
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 20Jan2007.)



Theorem  rexlimdvaa 2428* 
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by Mario Carneiro, 15Jun2016.)



Theorem  rexlimdv3a 2429* 
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). Frequentlyused variant of rexlimdv 2426. (Contributed by NM,
7Jun2015.)



Theorem  rexlimdvw 2430* 
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 18Jun2014.)



Theorem  rexlimddv 2431* 
Restricted existential elimination rule of natural deduction.
(Contributed by Mario Carneiro, 15Jun2016.)



Theorem  rexlimivv 2432* 
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 17Feb2004.)



Theorem  rexlimdvv 2433* 
Inference from Theorem 19.23 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 22Jul2004.)



Theorem  rexlimdvva 2434* 
Inference from Theorem 19.23 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 18Jun2014.)



Theorem  r19.26 2435 
Theorem 19.26 of [Margaris] p. 90 with
restricted quantifiers.
(Contributed by NM, 28Jan1997.) (Proof shortened by Andrew Salmon,
30May2011.)



Theorem  r19.262 2436 
Theorem 19.26 of [Margaris] p. 90 with 2
restricted quantifiers.
(Contributed by NM, 10Aug2004.)



Theorem  r19.263 2437 
Theorem 19.26 of [Margaris] p. 90 with 3
restricted quantifiers.
(Contributed by FL, 22Nov2010.)



Theorem  r19.26m 2438 
Theorem 19.26 of [Margaris] p. 90 with mixed
quantifiers. (Contributed by
NM, 22Feb2004.)



Theorem  ralbi 2439 
Distribute a restricted universal quantifier over a biconditional.
Theorem 19.15 of [Margaris] p. 90 with
restricted quantification.
(Contributed by NM, 6Oct2003.)



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, 21Jan2019.)



Theorem  ralbiim 2441 
Split a biconditional and distribute quantifier. (Contributed by NM,
3Jun2012.)



Theorem  r19.27av 2442* 
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, 3Jun2004.) (Proof shortened by Andrew Salmon,
30May2011.)



Theorem  r19.28av 2443* 
Restricted version of one direction of Theorem 19.28 of [Margaris]
p. 90. (The other direction doesn't hold when is empty.)
(Contributed by NM, 2Apr2004.)



Theorem  r19.29 2444 
Theorem 19.29 of [Margaris] p. 90 with
restricted quantifiers.
(Contributed by NM, 31Aug1999.) (Proof shortened by Andrew Salmon,
30May2011.)



Theorem  r19.29r 2445 
Variation of Theorem 19.29 of [Margaris] p. 90
with restricted
quantifiers. (Contributed by NM, 31Aug1999.)



Theorem  r19.29af2 2446 
A commonly used pattern based on r19.29 2444 (Contributed by Thierry
Arnoux, 17Dec2017.)



Theorem  r19.29af 2447* 
A commonly used pattern based on r19.29 2444 (Contributed by Thierry
Arnoux, 29Nov2017.)



Theorem  r19.29a 2448* 
A commonly used pattern based on r19.29 2444 (Contributed by Thierry
Arnoux, 22Nov2017.)



Theorem  r19.29d2r 2449 
Theorem 19.29 of [Margaris] p. 90 with two
restricted quantifiers,
deduction version (Contributed by Thierry Arnoux, 30Jan2017.)



Theorem  r19.29vva 2450* 
A commonly used pattern based on r19.29 2444, version with two restricted
quantifiers. (Contributed by Thierry Arnoux, 26Nov2017.)



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, 19Aug2018.)



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, 19Aug2018.)



Theorem  r19.32vdc 2453* 
Theorem 19.32 of [Margaris] p. 90 with
restricted quantifiers, where
is
decidable. (Contributed by Jim Kingdon, 4Jun2018.)

DECID 

Theorem  r19.351 2454 
Restricted quantifier version of 19.351 1512. (Contributed by Jim Kingdon,
4Jun2018.)



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
has at least one element, but in intuitionistic logic, that is not a
sufficient condition. (Contributed by NM, 22Oct2003.)



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 has at least
one element, but that is not sufficient in intuitionistic logic.
(Contributed by FL, 13May2012.) (Revised by Mario Carneiro,
11Dec2016.)



Theorem  r19.37av 2457* 
Restricted version of one direction of Theorem 19.37 of [Margaris]
p. 90. (Contributed by NM, 2Apr2004.)



Theorem  r19.40 2458 
Restricted quantifier version of Theorem 19.40 of [Margaris] p. 90.
(Contributed by NM, 2Apr2004.)



Theorem  r19.41 2459 
Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
(Contributed by NM, 1Nov2010.)



Theorem  r19.41v 2460* 
Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
(Contributed by NM, 17Dec2003.)



Theorem  r19.42v 2461* 
Restricted version of Theorem 19.42 of [Margaris] p. 90. (Contributed
by NM, 27May1998.)



Theorem  r19.43 2462 
Restricted version of Theorem 19.43 of [Margaris] p. 90. (Contributed by
NM, 27May1998.) (Proof rewritten by Jim Kingdon, 5Jun2018.)



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 is
empty. (Contributed by NM, 2Apr2004.)



Theorem  r19.45av 2464* 
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, 2Apr2004.)



Theorem  ralcomf 2465* 
Commutation of restricted quantifiers. (Contributed by Mario Carneiro,
14Oct2016.)



Theorem  rexcomf 2466* 
Commutation of restricted quantifiers. (Contributed by Mario Carneiro,
14Oct2016.)



Theorem  ralcom 2467* 
Commutation of restricted quantifiers. (Contributed by NM,
13Oct1999.) (Revised by Mario Carneiro, 14Oct2016.)



Theorem  rexcom 2468* 
Commutation of restricted quantifiers. (Contributed by NM,
19Nov1995.) (Revised by Mario Carneiro, 14Oct2016.)



Theorem  rexcom13 2469* 
Swap 1st and 3rd restricted existential quantifiers. (Contributed by
NM, 8Apr2015.)



Theorem  rexrot4 2470* 
Rotate existential restricted quantifiers twice. (Contributed by NM,
8Apr2015.)



Theorem  ralcom3 2471 
A commutative law for restricted quantifiers that swaps the domain of
the restriction. (Contributed by NM, 22Feb2004.)



Theorem  reean 2472* 
Rearrange existential quantifiers. (Contributed by NM, 27Oct2010.)
(Proof shortened by Andrew Salmon, 30May2011.)



Theorem  reeanv 2473* 
Rearrange existential quantifiers. (Contributed by NM, 9May1999.)



Theorem  3reeanv 2474* 
Rearrange three existential quantifiers. (Contributed by Jeff Madsen,
11Jun2010.)



Theorem  nfreu1 2475 
is not free in .
(Contributed by NM,
19Mar1997.)



Theorem  nfrmo1 2476 
is not free in .
(Contributed by NM,
16Jun2017.)



Theorem  nfreudxy 2477* 
Notfree deduction for restricted uniqueness. This is a version where
and are distinct. (Contributed
by Jim Kingdon,
6Jun2018.)



Theorem  nfreuxy 2478* 
Notfree for restricted uniqueness. This is a version where and
are distinct.
(Contributed by Jim Kingdon, 6Jun2018.)



Theorem  rabid 2479 
An "identity" law of concretion for restricted abstraction. Special
case
of Definition 2.1 of [Quine] p. 16.
(Contributed by NM, 9Oct2003.)



Theorem  rabid2 2480* 
An "identity" law for restricted class abstraction. (Contributed by
NM,
9Oct2003.) (Proof shortened by Andrew Salmon, 30May2011.)



Theorem  rabbi 2481 
Equivalent wff's correspond to equal restricted class abstractions.
Closed theorem form of rabbidva 2542. (Contributed by NM,
25Nov2013.)



Theorem  rabswap 2482 
Swap with a membership relation in a restricted class abstraction.
(Contributed by NM, 4Jul2005.)



Theorem  nfrab1 2483 
The abstraction variable in a restricted class abstraction isn't free.
(Contributed by NM, 19Mar1997.)



Theorem  nfrabxy 2484* 
A variable not free in a wff remains so in a restricted class
abstraction. (Contributed by Jim Kingdon, 19Jul2018.)



Theorem  reubida 2485 
Formulabuilding rule for restricted existential quantifier (deduction
rule). (Contributed by Mario Carneiro, 19Nov2016.)



Theorem  reubidva 2486* 
Formulabuilding rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 13Nov2004.)



Theorem  reubidv 2487* 
Formulabuilding rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 17Oct1996.)



Theorem  reubiia 2488 
Formulabuilding rule for restricted existential quantifier (inference
rule). (Contributed by NM, 14Nov2004.)



Theorem  reubii 2489 
Formulabuilding rule for restricted existential quantifier (inference
rule). (Contributed by NM, 22Oct1999.)



Theorem  rmobida 2490 
Formulabuilding rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 16Jun2017.)



Theorem  rmobidva 2491* 
Formulabuilding rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 16Jun2017.)



Theorem  rmobidv 2492* 
Formulabuilding rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 16Jun2017.)



Theorem  rmobiia 2493 
Formulabuilding rule for restricted existential quantifier (inference
rule). (Contributed by NM, 16Jun2017.)



Theorem  rmobii 2494 
Formulabuilding rule for restricted existential quantifier (inference
rule). (Contributed by NM, 16Jun2017.)



Theorem  raleqf 2495 
Equality theorem for restricted universal quantifier, with
boundvariable hypotheses instead of distinct variable restrictions.
(Contributed by NM, 7Mar2004.) (Revised by Andrew Salmon,
11Jul2011.)



Theorem  rexeqf 2496 
Equality theorem for restricted existential quantifier, with
boundvariable hypotheses instead of distinct variable restrictions.
(Contributed by NM, 9Oct2003.) (Revised by Andrew Salmon,
11Jul2011.)



Theorem  reueq1f 2497 
Equality theorem for restricted uniqueness quantifier, with
boundvariable hypotheses instead of distinct variable restrictions.
(Contributed by NM, 5Apr2004.) (Revised by Andrew Salmon,
11Jul2011.)



Theorem  rmoeq1f 2498 
Equality theorem for restricted uniqueness quantifier, with
boundvariable hypotheses instead of distinct variable restrictions.
(Contributed by Alexander van der Vekens, 17Jun2017.)



Theorem  raleq 2499* 
Equality theorem for restricted universal quantifier. (Contributed by
NM, 16Nov1995.)



Theorem  rexeq 2500* 
Equality theorem for restricted existential quantifier. (Contributed by
NM, 29Oct1995.)

