HomeHome New Foundations Explorer
Theorem List (p. 27 of 64)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 2601-2700   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremneanior 2601 A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
 
Theoremne3anior 2602 A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.)
 
Theoremneorian 2603 A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
 
Theoremnemtbir 2604 An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.)
   &       =>   
 
Theoremnelne1 2605 Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.)
 
Theoremnelne2 2606 Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.)
 
Theoremneleq1 2607 Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
 
Theoremneleq2 2608 Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
 
Theoremneleq12d 2609 Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.)
   &       =>   
 
Theoremnfne 2610 Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
 F/_   &     F/_   =>     F/
 
Theoremnfnel 2611 Bound-variable hypothesis builder for inequality. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
 F/_   &     F/_   =>     F/
 
Theoremnfned 2612 Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
 F/_   &     F/_   =>     F/
 
Theoremnfneld 2613 Bound-variable hypothesis builder for inequality. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
 F/_   &     F/_   =>     F/
 
2.1.5  Restricted quantification
 
Syntaxwral 2614 Extend wff notation to include restricted universal quantification.
 
Syntaxwrex 2615 Extend wff notation to include restricted existential quantification.
 
Syntaxwreu 2616 Extend wff notation to include restricted existential uniqueness.
 
Syntaxwrmo 2617 Extend wff notation to include restricted "at most one."
 
Syntaxcrab 2618 Extend class notation to include the restricted class abstraction (class builder).
 
Definitiondf-ral 2619 Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)
 
Definitiondf-rex 2620 Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)
 
Definitiondf-reu 2621 Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
 
Definitiondf-rmo 2622 Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
 
Definitiondf-rab 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, 22-Nov-1994.)
 
Theoremralnex 2624 Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
 
Theoremrexnal 2625 Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
 
Theoremdfral2 2626 Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
 
Theoremdfrex2 2627 Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
 
Theoremralbida 2628 Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Oct-2003.)

 F/   &       =>   
 
Theoremrexbida 2629 Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 6-Oct-2003.)

 F/   &       =>   
 
Theoremralbidva 2630* Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 4-Mar-1997.)
   =>   
 
Theoremrexbidva 2631* Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 9-Mar-1997.)
   =>   
 
Theoremralbid 2632 Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.)

 F/   &       =>   
 
Theoremrexbid 2633 Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.)

 F/   &       =>   
 
Theoremralbidv 2634* Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
   =>   
 
Theoremrexbidv 2635* Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
   =>   
 
Theoremralbidv2 2636* Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Apr-1997.)
   =>   
 
Theoremrexbidv2 2637* Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 22-May-1999.)
   =>   
 
Theoremralbii 2638 Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)
   =>   
 
Theoremrexbii 2639 Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)
   =>   
 
Theorem2ralbii 2640 Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
   =>   
 
Theorem2rexbii 2641 Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)
   =>   
 
Theoremralbii2 2642 Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.)
   =>   
 
Theoremrexbii2 2643 Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.)
   =>   
 
Theoremraleqbii 2644 Equality deduction for restricted universal quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
   &       =>   
 
Theoremrexeqbii 2645 Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
   &       =>   
 
Theoremralbiia 2646 Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.)
   =>   
 
Theoremrexbiia 2647 Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.)
   =>   
 
Theorem2rexbiia 2648* Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
   =>   
 
Theoremr2alf 2649* Double restricted universal quantification. (Contributed by Mario Carneiro, 14-Oct-2016.)
 F/_   =>   
 
Theoremr2exf 2650* Double restricted existential quantification. (Contributed by Mario Carneiro, 14-Oct-2016.)
 F/_   =>   
 
Theoremr2al 2651* Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.)
 
Theoremr2ex 2652* Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.)
 
Theorem2ralbida 2653* Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 24-Feb-2004.)

 F/   &     F/   &       =>   
 
Theorem2ralbidva 2654* Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.)
   =>   
 
Theorem2rexbidva 2655* Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 15-Dec-2004.)
   =>   
 
Theorem2ralbidv 2656* Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)
   =>   
 
Theorem2rexbidv 2657* Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
   =>   
 
Theoremrexralbidv 2658* Formula-building rule for restricted quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
   =>   
 
Theoremralinexa 2659 A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.)
 
Theoremrexanali 2660 A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.)
 
Theoremrisset 2661* Two ways to say " belongs to ." (Contributed by NM, 22-Nov-1994.)
 
Theoremhbral 2662 Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by David Abernethy, 13-Dec-2009.)
   &       =>   
 
Theoremhbra1 2663 is not free in . (Contributed by NM, 18-Oct-1996.)
 
Theoremnfra1 2664 is not free in . (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)

 F/
 
Theoremnfrald 2665 Deduction version of nfral 2667. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.)

 F/   &     F/_   &     F/   =>     F/
 
Theoremnfrexd 2666 Deduction version of nfrex 2669. (Contributed by Mario Carneiro, 14-Oct-2016.)

 F/   &     F/_   &     F/   =>     F/
 
Theoremnfral 2667 Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.)
 F/_   &     F/   =>    
 F/
 
Theoremnfra2 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 31-Dec-2011. (Contributed by NM, 31-Dec-2011.)

 F/
 
Theoremnfrex 2669 Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.)
 F/_   &     F/   =>    
 F/
 
Theoremnfre1 2670 is not free in . (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)

 F/
 
Theoremr3al 2671* Triple restricted universal quantification. (Contributed by NM, 19-Nov-1995.)
 
Theoremalral 2672 Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.)
 
Theoremrexex 2673 Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)
 
Theoremrsp 2674 Restricted specialization. (Contributed by NM, 17-Oct-1996.)
 
Theoremrspe 2675 Restricted specialization. (Contributed by NM, 12-Oct-1999.)
 
Theoremrsp2 2676 Restricted specialization. (Contributed by NM, 11-Feb-1997.)
 
Theoremrsp2e 2677 Restricted specialization. (Contributed by FL, 4-Jun-2012.)
 
Theoremrspec 2678 Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
   =>   
 
Theoremrgen 2679 Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
   =>   
 
Theoremrgen2a 2680* Generalization rule for restricted quantification. Note that and needn't be distinct (and illustrates the use of dvelim 2016). (Contributed by NM, 23-Nov-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.
   =>   
 
Theoremrgenw 2681 Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
   =>   
 
Theoremrgen2w 2682 Generalization rule for restricted quantification. Note that and needn't be distinct. (Contributed by NM, 18-Jun-2014.)
   =>   
 
Theoremmprg 2683 Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.)
   &       =>   
 
Theoremmprgbir 2684 Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)
   &       =>   
 
Theoremralim 2685 Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.)
 
Theoremralimi2 2686 Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.)
   =>   
 
Theoremralimia 2687 Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)
   =>   
 
Theoremralimiaa 2688 Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.)
   =>   
 
Theoremralimi 2689 Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
   =>   
 
Theoremral2imi 2690 Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.)
   =>   
 
Theoremralimdaa 2691 Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-Sep-2003.)

 F/   &       =>   
 
Theoremralimdva 2692* Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
   =>   
 
Theoremralimdv 2693* Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 8-Oct-2003.)
   =>   
 
Theoremralimdv2 2694* Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.)
   =>   
 
Theoremralrimi 2695 Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.)

 F/   &       =>   
 
Theoremralrimiv 2696* Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.)
   =>   
 
Theoremralrimiva 2697* Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)
   =>   
 
Theoremralrimivw 2698* Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
   =>   
 
Theoremr19.21t 2699 Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers (closed theorem version). (Contributed by NM, 1-Mar-2008.)
 F/
 
Theoremr19.21 2700 Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers. (Contributed by Scott Fenton, 30-Mar-2011.)

 F/   =>   
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6338
  Copyright terms: Public domain < Previous  Next >