Type  Label  Description 
Statement 

Theorem  ralinexa 2401 
A transformation of restricted quantifiers and logical connectives.
(Contributed by NM, 4Sep2005.)



Theorem  risset 2402* 
Two ways to say "
belongs to ."
(Contributed by NM,
22Nov1994.)



Theorem  hbral 2403 
Boundvariable hypothesis builder for restricted quantification.
(Contributed by NM, 1Sep1999.) (Revised by David Abernethy,
13Dec2009.)



Theorem  hbra1 2404 
is not free in .
(Contributed by NM,
18Oct1996.)



Theorem  nfra1 2405 
is not free in .
(Contributed by NM, 18Oct1996.)
(Revised by Mario Carneiro, 7Oct2016.)



Theorem  nfraldxy 2406* 
Notfree for restricted universal quantification where and
are distinct. See nfraldya 2408 for a version with and
distinct instead. (Contributed by Jim Kingdon, 29May2018.)



Theorem  nfrexdxy 2407* 
Notfree for restricted existential quantification where and
are distinct. See nfrexdya 2409 for a version with and
distinct instead. (Contributed by Jim Kingdon, 30May2018.)



Theorem  nfraldya 2408* 
Notfree for restricted universal quantification where and
are distinct. See nfraldxy 2406 for a version with and
distinct instead. (Contributed by Jim Kingdon, 30May2018.)



Theorem  nfrexdya 2409* 
Notfree for restricted existential quantification where and
are distinct. See nfrexdxy 2407 for a version with and
distinct instead. (Contributed by Jim Kingdon, 30May2018.)



Theorem  nfralxy 2410* 
Notfree for restricted universal quantification where and
are distinct. See nfralya 2412 for a version with and distinct
instead. (Contributed by Jim Kingdon, 30May2018.)



Theorem  nfrexxy 2411* 
Notfree for restricted existential quantification where and
are distinct. See nfrexya 2413 for a version with and distinct
instead. (Contributed by Jim Kingdon, 30May2018.)



Theorem  nfralya 2412* 
Notfree for restricted universal quantification where and
are distinct. See nfralxy 2410 for a version with and distinct
instead. (Contributed by Jim Kingdon, 3Jun2018.)



Theorem  nfrexya 2413* 
Notfree for restricted existential quantification where and
are distinct. See nfrexxy 2411 for a version with and distinct
instead. (Contributed by Jim Kingdon, 3Jun2018.)



Theorem  nfra2xy 2414* 
Notfree given two restricted quantifiers. (Contributed by Jim Kingdon,
20Aug2018.)



Theorem  nfre1 2415 
is not free in .
(Contributed by NM, 19Mar1997.)
(Revised by Mario Carneiro, 7Oct2016.)



Theorem  r3al 2416* 
Triple restricted universal quantification. (Contributed by NM,
19Nov1995.)



Theorem  alral 2417 
Universal quantification implies restricted quantification. (Contributed
by NM, 20Oct2006.)



Theorem  rexex 2418 
Restricted existence implies existence. (Contributed by NM,
11Nov1995.)



Theorem  rsp 2419 
Restricted specialization. (Contributed by NM, 17Oct1996.)



Theorem  rspe 2420 
Restricted specialization. (Contributed by NM, 12Oct1999.)



Theorem  rsp2 2421 
Restricted specialization. (Contributed by NM, 11Feb1997.)



Theorem  rsp2e 2422 
Restricted specialization. (Contributed by FL, 4Jun2012.)



Theorem  rspec 2423 
Specialization rule for restricted quantification. (Contributed by NM,
19Nov1994.)



Theorem  rgen 2424 
Generalization rule for restricted quantification. (Contributed by NM,
19Nov1994.)



Theorem  rgen2a 2425* 
Generalization rule for restricted quantification. Note that and
needn't be
distinct (and illustrates the use of dvelimor 1939).
(Contributed by NM, 23Nov1994.) (Proof rewritten by Jim Kingdon,
1Jun2018.)



Theorem  rgenw 2426 
Generalization rule for restricted quantification. (Contributed by NM,
18Jun2014.)



Theorem  rgen2w 2427 
Generalization rule for restricted quantification. Note that and
needn't be
distinct. (Contributed by NM, 18Jun2014.)



Theorem  mprg 2428 
Modus ponens combined with restricted generalization. (Contributed by
NM, 10Aug2004.)



Theorem  mprgbir 2429 
Modus ponens on biconditional combined with restricted generalization.
(Contributed by NM, 21Mar2004.)



Theorem  ralim 2430 
Distribution of restricted quantification over implication. (Contributed
by NM, 9Feb1997.)



Theorem  ralimi2 2431 
Inference quantifying both antecedent and consequent. (Contributed by
NM, 22Feb2004.)



Theorem  ralimia 2432 
Inference quantifying both antecedent and consequent. (Contributed by
NM, 19Jul1996.)



Theorem  ralimiaa 2433 
Inference quantifying both antecedent and consequent. (Contributed by
NM, 4Aug2007.)



Theorem  ralimi 2434 
Inference quantifying both antecedent and consequent, with strong
hypothesis. (Contributed by NM, 4Mar1997.)



Theorem  ral2imi 2435 
Inference quantifying antecedent, nested antecedent, and consequent,
with a strong hypothesis. (Contributed by NM, 19Dec2006.)



Theorem  ralimdaa 2436 
Deduction quantifying both antecedent and consequent, based on Theorem
19.20 of [Margaris] p. 90.
(Contributed by NM, 22Sep2003.)



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



Theorem  ralimdv 2438* 
Deduction quantifying both antecedent and consequent, based on Theorem
19.20 of [Margaris] p. 90.
(Contributed by NM, 8Oct2003.)



Theorem  ralimdv2 2439* 
Inference quantifying both antecedent and consequent. (Contributed by
NM, 1Feb2005.)



Theorem  ralrimi 2440 
Inference from Theorem 19.21 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 10Oct1999.)



Theorem  ralrimiv 2441* 
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 22Nov1994.)



Theorem  ralrimiva 2442* 
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 2Jan2006.)



Theorem  ralrimivw 2443* 
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 18Jun2014.)



Theorem  r19.21t 2444 
Theorem 19.21 of [Margaris] p. 90 with
restricted quantifiers (closed
theorem version). (Contributed by NM, 1Mar2008.)



Theorem  r19.21 2445 
Theorem 19.21 of [Margaris] p. 90 with
restricted quantifiers.
(Contributed by Scott Fenton, 30Mar2011.)



Theorem  r19.21v 2446* 
Theorem 19.21 of [Margaris] p. 90 with
restricted quantifiers.
(Contributed by NM, 15Oct2003.) (Proof shortened by Andrew Salmon,
30May2011.)



Theorem  ralrimd 2447 
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 16Feb2004.)



Theorem  ralrimdv 2448* 
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 27May1998.)



Theorem  ralrimdva 2449* 
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 2Feb2008.)



Theorem  ralrimivv 2450* 
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version with double quantification.) (Contributed by NM,
24Jul2004.)



Theorem  ralrimivva 2451* 
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version with double quantification.) (Contributed by Jeff
Madsen, 19Jun2011.)



Theorem  ralrimivvva 2452* 
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version with triple quantification.) (Contributed by Mario
Carneiro, 9Jul2014.)



Theorem  ralrimdvv 2453* 
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version with double quantification.) (Contributed by NM,
1Jun2005.)



Theorem  ralrimdvva 2454* 
Inference from Theorem 19.21 of [Margaris] p.
90. (Restricted
quantifier version with double quantification.) (Contributed by NM,
2Feb2008.)



Theorem  rgen2 2455* 
Generalization rule for restricted quantification. (Contributed by NM,
30May1999.)



Theorem  rgen3 2456* 
Generalization rule for restricted quantification. (Contributed by NM,
12Jan2008.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  reximddv 2472* 
Deduction from Theorem 19.22 of [Margaris] p.
90. (Contributed by
Thierry Arnoux, 7Dec2016.)



Theorem  reximddv2 2473* 
Double deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed
by Thierry Arnoux, 15Dec2019.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  rexbi 2498 
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 2499 
Split a biconditional and distribute quantifier. (Contributed by NM,
3Jun2012.)



Theorem  r19.27av 2500* 
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.)

