Type  Label  Description 
Statement 

Theorem  neanior 2601 
A De Morgan's law for inequality. (Contributed by NM, 18May2007.)



Theorem  ne3anior 2602 
A De Morgan's law for inequality. (Contributed by NM, 30Sep2013.)



Theorem  neorian 2603 
A De Morgan's law for inequality. (Contributed by NM, 18May2007.)



Theorem  nemtbir 2604 
An inference from an inequality, related to modus tollens. (Contributed
by NM, 13Apr2007.)



Theorem  nelne1 2605 
Two classes are different if they don't contain the same element.
(Contributed by NM, 3Feb2012.)



Theorem  nelne2 2606 
Two classes are different if they don't belong to the same class.
(Contributed by NM, 25Jun2012.)



Theorem  neleq1 2607 
Equality theorem for negated membership. (Contributed by NM,
20Nov1994.)



Theorem  neleq2 2608 
Equality theorem for negated membership. (Contributed by NM,
20Nov1994.)



Theorem  neleq12d 2609 
Equality theorem for negated membership. (Contributed by FL,
10Aug2016.)



Theorem  nfne 2610 
Boundvariable hypothesis builder for inequality. (Contributed by NM,
10Nov2007.) (Revised by Mario Carneiro, 7Oct2016.)



Theorem  nfnel 2611 
Boundvariable hypothesis builder for inequality. (Contributed by David
Abernethy, 26Jun2011.) (Revised by Mario Carneiro, 7Oct2016.)



Theorem  nfned 2612 
Boundvariable hypothesis builder for inequality. (Contributed by NM,
10Nov2007.) (Revised by Mario Carneiro, 7Oct2016.)



Theorem  nfneld 2613 
Boundvariable hypothesis builder for inequality. (Contributed by David
Abernethy, 26Jun2011.) (Revised by Mario Carneiro, 7Oct2016.)



2.1.5 Restricted quantification


Syntax  wral 2614 
Extend wff notation to include restricted universal quantification.



Syntax  wrex 2615 
Extend wff notation to include restricted existential quantification.



Syntax  wreu 2616 
Extend wff notation to include restricted existential uniqueness.



Syntax  wrmo 2617 
Extend wff notation to include restricted "at most one."



Syntax  crab 2618 
Extend class notation to include the restricted class abstraction (class
builder).



Definition  dfral 2619 
Define restricted universal quantification. Special case of Definition
4.15(3) of [TakeutiZaring] p. 22.
(Contributed by NM, 19Aug1993.)



Definition  dfrex 2620 
Define restricted existential quantification. Special case of Definition
4.15(4) of [TakeutiZaring] p. 22.
(Contributed by NM, 30Aug1993.)



Definition  dfreu 2621 
Define restricted existential uniqueness. (Contributed by NM,
22Nov1994.)



Definition  dfrmo 2622 
Define restricted "at most one". (Contributed by NM, 16Jun2017.)



Definition  dfrab 2623 
Define a restricted class abstraction (class builder), which is the class
of all in such that is true. Definition
of
[TakeutiZaring] p. 20. (Contributed
by NM, 22Nov1994.)



Theorem  ralnex 2624 
Relationship between restricted universal and existential quantifiers.
(Contributed by NM, 21Jan1997.)



Theorem  rexnal 2625 
Relationship between restricted universal and existential quantifiers.
(Contributed by NM, 21Jan1997.)



Theorem  dfral2 2626 
Relationship between restricted universal and existential quantifiers.
(Contributed by NM, 21Jan1997.)



Theorem  dfrex2 2627 
Relationship between restricted universal and existential quantifiers.
(Contributed by NM, 21Jan1997.)



Theorem  ralbida 2628 
Formulabuilding rule for restricted universal quantifier (deduction
rule). (Contributed by NM, 6Oct2003.)



Theorem  rexbida 2629 
Formulabuilding rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 6Oct2003.)



Theorem  ralbidva 2630* 
Formulabuilding rule for restricted universal quantifier (deduction
rule). (Contributed by NM, 4Mar1997.)



Theorem  rexbidva 2631* 
Formulabuilding rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 9Mar1997.)



Theorem  ralbid 2632 
Formulabuilding rule for restricted universal quantifier (deduction
rule). (Contributed by NM, 27Jun1998.)



Theorem  rexbid 2633 
Formulabuilding rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 27Jun1998.)



Theorem  ralbidv 2634* 
Formulabuilding rule for restricted universal quantifier (deduction
rule). (Contributed by NM, 20Nov1994.)



Theorem  rexbidv 2635* 
Formulabuilding rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 20Nov1994.)



Theorem  ralbidv2 2636* 
Formulabuilding rule for restricted universal quantifier (deduction
rule). (Contributed by NM, 6Apr1997.)



Theorem  rexbidv2 2637* 
Formulabuilding rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 22May1999.)



Theorem  ralbii 2638 
Inference adding restricted universal quantifier to both sides of an
equivalence. (Contributed by NM, 23Nov1994.) (Revised by Mario
Carneiro, 17Oct2016.)



Theorem  rexbii 2639 
Inference adding restricted existential quantifier to both sides of an
equivalence. (Contributed by NM, 23Nov1994.) (Revised by Mario
Carneiro, 17Oct2016.)



Theorem  2ralbii 2640 
Inference adding two restricted universal quantifiers to both sides of
an equivalence. (Contributed by NM, 1Aug2004.)



Theorem  2rexbii 2641 
Inference adding two restricted existential quantifiers to both sides of
an equivalence. (Contributed by NM, 11Nov1995.)



Theorem  ralbii2 2642 
Inference adding different restricted universal quantifiers to each side
of an equivalence. (Contributed by NM, 15Aug2005.)



Theorem  rexbii2 2643 
Inference adding different restricted existential quantifiers to each
side of an equivalence. (Contributed by NM, 4Feb2004.)



Theorem  raleqbii 2644 
Equality deduction for restricted universal quantifier, changing both
formula and quantifier domain. Inference form. (Contributed by David
Moews, 1May2017.)



Theorem  rexeqbii 2645 
Equality deduction for restricted existential quantifier, changing both
formula and quantifier domain. Inference form. (Contributed by David
Moews, 1May2017.)



Theorem  ralbiia 2646 
Inference adding restricted universal quantifier to both sides of an
equivalence. (Contributed by NM, 26Nov2000.)



Theorem  rexbiia 2647 
Inference adding restricted existential quantifier to both sides of an
equivalence. (Contributed by NM, 26Oct1999.)



Theorem  2rexbiia 2648* 
Inference adding two restricted existential quantifiers to both sides of
an equivalence. (Contributed by NM, 1Aug2004.)



Theorem  r2alf 2649* 
Double restricted universal quantification. (Contributed by Mario
Carneiro, 14Oct2016.)



Theorem  r2exf 2650* 
Double restricted existential quantification. (Contributed by Mario
Carneiro, 14Oct2016.)



Theorem  r2al 2651* 
Double restricted universal quantification. (Contributed by NM,
19Nov1995.)



Theorem  r2ex 2652* 
Double restricted existential quantification. (Contributed by NM,
11Nov1995.)



Theorem  2ralbida 2653* 
Formulabuilding rule for restricted universal quantifier (deduction
rule). (Contributed by NM, 24Feb2004.)



Theorem  2ralbidva 2654* 
Formulabuilding rule for restricted universal quantifiers (deduction
rule). (Contributed by NM, 4Mar1997.)



Theorem  2rexbidva 2655* 
Formulabuilding rule for restricted existential quantifiers (deduction
rule). (Contributed by NM, 15Dec2004.)



Theorem  2ralbidv 2656* 
Formulabuilding rule for restricted universal quantifiers (deduction
rule). (Contributed by NM, 28Jan2006.) (Revised by Szymon
Jaroszewicz, 16Mar2007.)



Theorem  2rexbidv 2657* 
Formulabuilding rule for restricted existential quantifiers (deduction
rule). (Contributed by NM, 28Jan2006.)



Theorem  rexralbidv 2658* 
Formulabuilding rule for restricted quantifiers (deduction rule).
(Contributed by NM, 28Jan2006.)



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



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



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



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



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



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



Theorem  nfrald 2665 
Deduction version of nfral 2667. (Contributed by NM, 15Feb2013.)
(Revised by Mario Carneiro, 7Oct2016.)



Theorem  nfrexd 2666 
Deduction version of nfrex 2669. (Contributed by Mario Carneiro,
14Oct2016.)



Theorem  nfral 2667 
Boundvariable hypothesis builder for restricted quantification.
(Contributed by NM, 1Sep1999.) (Revised by Mario Carneiro,
7Oct2016.)



Theorem  nfra2 2668* 
Similar to Lemma 24 of [Monk2] p. 114, except the
quantification of the
antecedent is restricted. Derived automatically from hbra2VD in
set.mm. Contributed by Alan Sare 31Dec2011. (Contributed by NM,
31Dec2011.)



Theorem  nfrex 2669 
Boundvariable hypothesis builder for restricted quantification.
(Contributed by NM, 1Sep1999.) (Revised by Mario Carneiro,
7Oct2016.)



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



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



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



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



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



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



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



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



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



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



Theorem  rgen2a 2680* 
Generalization rule for restricted quantification. Note that and
needn't be
distinct (and illustrates the use of dvelim 2016).
(Contributed by NM, 23Nov1994.) (Proof shortened by Andrew Salmon,
25May2011.) (Proof modification is discouraged.



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

