HomeHome Intuitionistic Logic Explorer
Theorem List (p. 24 of 94)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 2301-2400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Syntaxwrex 2301 Extend wff notation to include restricted existential quantification.
 
Syntaxwreu 2302 Extend wff notation to include restricted existential uniqueness.
 
Syntaxwrmo 2303 Extend wff notation to include restricted "at most one."
 
Syntaxcrab 2304 Extend class notation to include the restricted class abstraction (class builder).
 {  |  }
 
Definitiondf-ral 2305 Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)
 
Definitiondf-rex 2306 Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)
 
Definitiondf-reu 2307 Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
 
Definitiondf-rmo 2308 Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
 
Definitiondf-rab 2309 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 2310 Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
 
Theoremrexnalim 2311 Relationship between restricted universal and existential quantifiers. In classical logic this would be a biconditional. (Contributed by Jim Kingdon, 17-Aug-2018.)
 
Theoremralexim 2312 Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)
 
Theoremrexalim 2313 Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)
 
Theoremralbida 2314 Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Oct-2003.)

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

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

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

 F/   &       =>   
 
Theoremralbidv 2320* Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
   =>   
 
Theoremrexbidv 2321* Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
   =>   
 
Theoremralbidv2 2322* Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Apr-1997.)
   =>   
 
Theoremrexbidv2 2323* Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 22-May-1999.)
   =>   
 
Theoremralbii 2324 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 2325 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 2326 Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
   =>   
 
Theorem2rexbii 2327 Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)
   =>   
 
Theoremralbii2 2328 Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.)
   =>   
 
Theoremrexbii2 2329 Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.)
   =>   
 
Theoremraleqbii 2330 Equality deduction for restricted universal quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
   &       =>   
 
Theoremrexeqbii 2331 Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
   &       =>   
 
Theoremralbiia 2332 Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.)
   =>   
 
Theoremrexbiia 2333 Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.)
   =>   
 
Theorem2rexbiia 2334* Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
   =>   
 
Theoremr2alf 2335* Double restricted universal quantification. (Contributed by Mario Carneiro, 14-Oct-2016.)
 F/_   =>   
 
Theoremr2exf 2336* Double restricted existential quantification. (Contributed by Mario Carneiro, 14-Oct-2016.)
 F/_   =>   
 
Theoremr2al 2337* Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.)
 
Theoremr2ex 2338* Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.)
 
Theorem2ralbida 2339* Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 24-Feb-2004.)

 F/   &     F/   &       =>   
 
Theorem2ralbidva 2340* Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.)
   =>   
 
Theorem2rexbidva 2341* Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 15-Dec-2004.)
   =>   
 
Theorem2ralbidv 2342* Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)
   =>   
 
Theorem2rexbidv 2343* Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
   =>   
 
Theoremrexralbidv 2344* Formula-building rule for restricted quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
   =>   
 
Theoremralinexa 2345 A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.)
 
Theoremrisset 2346* Two ways to say " belongs to ." (Contributed by NM, 22-Nov-1994.)
 
Theoremhbral 2347 Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by David Abernethy, 13-Dec-2009.)
   &       =>   
 
Theoremhbra1 2348 is not free in . (Contributed by NM, 18-Oct-1996.)
 
Theoremnfra1 2349 is not free in . (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)

 F/
 
Theoremnfraldxy 2350* Not-free for restricted universal quantification where and are distinct. See nfraldya 2352 for a version with and distinct instead. (Contributed by Jim Kingdon, 29-May-2018.)

 F/   &     F/_   &     F/   =>     F/
 
Theoremnfrexdxy 2351* Not-free for restricted existential quantification where and are distinct. See nfrexdya 2353 for a version with and distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)

 F/   &     F/_   &     F/   =>     F/
 
Theoremnfraldya 2352* Not-free for restricted universal quantification where and are distinct. See nfraldxy 2350 for a version with and distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)

 F/   &     F/_   &     F/   =>     F/
 
Theoremnfrexdya 2353* Not-free for restricted existential quantification where and are distinct. See nfrexdxy 2351 for a version with and distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)

 F/   &     F/_   &     F/   =>     F/
 
Theoremnfralxy 2354* Not-free for restricted universal quantification where and are distinct. See nfralya 2356 for a version with and distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
 F/_   &     F/   =>    
 F/
 
Theoremnfrexxy 2355* Not-free for restricted existential quantification where and are distinct. See nfrexya 2357 for a version with and distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
 F/_   &     F/   =>    
 F/
 
Theoremnfralya 2356* Not-free for restricted universal quantification where and are distinct. See nfralxy 2354 for a version with and distinct instead. (Contributed by Jim Kingdon, 3-Jun-2018.)
 F/_   &     F/   =>    
 F/
 
Theoremnfrexya 2357* Not-free for restricted existential quantification where and are distinct. See nfrexxy 2355 for a version with and distinct instead. (Contributed by Jim Kingdon, 3-Jun-2018.)
 F/_   &     F/   =>    
 F/
 
Theoremnfra2xy 2358* Not-free given two restricted quantifiers. (Contributed by Jim Kingdon, 20-Aug-2018.)

 F/
 
Theoremnfre1 2359 is not free in . (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)

 F/
 
Theoremr3al 2360* Triple restricted universal quantification. (Contributed by NM, 19-Nov-1995.)
 C  C
 
Theoremalral 2361 Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.)
 
Theoremrexex 2362 Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)
 
Theoremrsp 2363 Restricted specialization. (Contributed by NM, 17-Oct-1996.)
 
Theoremrspe 2364 Restricted specialization. (Contributed by NM, 12-Oct-1999.)
 
Theoremrsp2 2365 Restricted specialization. (Contributed by NM, 11-Feb-1997.)
 
Theoremrsp2e 2366 Restricted specialization. (Contributed by FL, 4-Jun-2012.)
 
Theoremrspec 2367 Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
   =>   
 
Theoremrgen 2368 Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
   =>   
 
Theoremrgen2a 2369* Generalization rule for restricted quantification. Note that and needn't be distinct (and illustrates the use of dvelimor 1891). (Contributed by NM, 23-Nov-1994.) (Proof rewritten by Jim Kingdon, 1-Jun-2018.)
   =>   
 
Theoremrgenw 2370 Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
   =>   
 
Theoremrgen2w 2371 Generalization rule for restricted quantification. Note that and needn't be distinct. (Contributed by NM, 18-Jun-2014.)
   =>   
 
Theoremmprg 2372 Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.)
   &       =>   
 
Theoremmprgbir 2373 Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)
   &       =>   
 
Theoremralim 2374 Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.)
 
Theoremralimi2 2375 Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.)
   =>   
 
Theoremralimia 2376 Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)
   =>   
 
Theoremralimiaa 2377 Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.)
   =>   
 
Theoremralimi 2378 Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
   =>   
 
Theoremral2imi 2379 Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.)
   =>   
 
Theoremralimdaa 2380 Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-Sep-2003.)

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

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

 F/   =>   
 
Theoremr19.21v 2390* Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
 
Theoremralrimd 2391 Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 16-Feb-2004.)

 F/   &     F/   &       =>   
 
Theoremralrimdv 2392* Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 27-May-1998.)
   =>   
 
Theoremralrimdva 2393* Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.)
   =>   
 
Theoremralrimivv 2394* Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.)
   =>   
 
Theoremralrimivva 2395* Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.)
   =>   
 
Theoremralrimivvva 2396* Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with triple quantification.) (Contributed by Mario Carneiro, 9-Jul-2014.)
 C    =>     C
 
Theoremralrimdvv 2397* Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 1-Jun-2005.)
   =>   
 
Theoremralrimdvva 2398* Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 2-Feb-2008.)
   =>   
 
Theoremrgen2 2399* Generalization rule for restricted quantification. (Contributed by NM, 30-May-1999.)
   =>   
 
Theoremrgen3 2400* Generalization rule for restricted quantification. (Contributed by NM, 12-Jan-2008.)
 C    =>     C
    < 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-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9381
  Copyright terms: Public domain < Previous  Next >