Home Intuitionistic Logic ExplorerTheorem List (p. 24 of 102) < 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

Theoremneleq1 2301 Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)

Theoremneleq2 2302 Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)

Theoremneleq12d 2303 Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.)

Theoremnfnel 2304 Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)

Theoremnfneld 2305 Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)

2.1.5  Restricted quantification

Syntaxwral 2306 Extend wff notation to include restricted universal quantification.

Syntaxwrex 2307 Extend wff notation to include restricted existential quantification.

Syntaxwreu 2308 Extend wff notation to include restricted existential uniqueness.

Syntaxwrmo 2309 Extend wff notation to include restricted "at most one."

Syntaxcrab 2310 Extend class notation to include the restricted class abstraction (class builder).

Definitiondf-ral 2311 Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)

Definitiondf-rex 2312 Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)

Definitiondf-reu 2313 Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)

Definitiondf-rmo 2314 Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)

Definitiondf-rab 2315 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 2316 Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)

Theoremrexnalim 2317 Relationship between restricted universal and existential quantifiers. In classical logic this would be a biconditional. (Contributed by Jim Kingdon, 17-Aug-2018.)

Theoremralexim 2318 Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)

Theoremrexalim 2319 Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)

Theoremralbida 2320 Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Oct-2003.)

Theoremrexbida 2321 Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 6-Oct-2003.)

Theoremralbidva 2322* Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 4-Mar-1997.)

Theoremrexbidva 2323* Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 9-Mar-1997.)

Theoremralbid 2324 Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.)

Theoremrexbid 2325 Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.)

Theoremralbidv 2326* Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)

Theoremrexbidv 2327* Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)

Theoremralbidv2 2328* Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Apr-1997.)

Theoremrexbidv2 2329* Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 22-May-1999.)

Theoremralbii 2330 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 2331 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 2332 Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)

Theorem2rexbii 2333 Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)

Theoremralbii2 2334 Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.)

Theoremrexbii2 2335 Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.)

Theoremraleqbii 2336 Equality deduction for restricted universal quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)

Theoremrexeqbii 2337 Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)

Theoremralbiia 2338 Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.)

Theoremrexbiia 2339 Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.)

Theorem2rexbiia 2340* Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)

Theoremr2alf 2341* Double restricted universal quantification. (Contributed by Mario Carneiro, 14-Oct-2016.)

Theoremr2exf 2342* Double restricted existential quantification. (Contributed by Mario Carneiro, 14-Oct-2016.)

Theoremr2al 2343* Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.)

Theoremr2ex 2344* Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.)

Theorem2ralbida 2345* Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 24-Feb-2004.)

Theorem2ralbidva 2346* Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.)

Theorem2rexbidva 2347* Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 15-Dec-2004.)

Theorem2ralbidv 2348* Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)

Theorem2rexbidv 2349* Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)

Theoremrexralbidv 2350* Formula-building rule for restricted quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)

Theoremralinexa 2351 A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.)

Theoremrisset 2352* Two ways to say " belongs to ." (Contributed by NM, 22-Nov-1994.)

Theoremhbral 2353 Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by David Abernethy, 13-Dec-2009.)

Theoremhbra1 2354 is not free in . (Contributed by NM, 18-Oct-1996.)

Theoremnfra1 2355 is not free in . (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)

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

Theoremnfrexdxy 2357* Not-free for restricted existential quantification where and are distinct. See nfrexdya 2359 for a version with and distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)

Theoremnfraldya 2358* Not-free for restricted universal quantification where and are distinct. See nfraldxy 2356 for a version with and distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)

Theoremnfrexdya 2359* Not-free for restricted existential quantification where and are distinct. See nfrexdxy 2357 for a version with and distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)

Theoremnfralxy 2360* Not-free for restricted universal quantification where and are distinct. See nfralya 2362 for a version with and distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)

Theoremnfrexxy 2361* Not-free for restricted existential quantification where and are distinct. See nfrexya 2363 for a version with and distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)

Theoremnfralya 2362* Not-free for restricted universal quantification where and are distinct. See nfralxy 2360 for a version with and distinct instead. (Contributed by Jim Kingdon, 3-Jun-2018.)

Theoremnfrexya 2363* Not-free for restricted existential quantification where and are distinct. See nfrexxy 2361 for a version with and distinct instead. (Contributed by Jim Kingdon, 3-Jun-2018.)

Theoremnfra2xy 2364* Not-free given two restricted quantifiers. (Contributed by Jim Kingdon, 20-Aug-2018.)

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

Theoremr3al 2366* Triple restricted universal quantification. (Contributed by NM, 19-Nov-1995.)

Theoremalral 2367 Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.)

Theoremrexex 2368 Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)

Theoremrsp 2369 Restricted specialization. (Contributed by NM, 17-Oct-1996.)

Theoremrspe 2370 Restricted specialization. (Contributed by NM, 12-Oct-1999.)

Theoremrsp2 2371 Restricted specialization. (Contributed by NM, 11-Feb-1997.)

Theoremrsp2e 2372 Restricted specialization. (Contributed by FL, 4-Jun-2012.)

Theoremrspec 2373 Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)

Theoremrgen 2374 Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)

Theoremrgen2a 2375* Generalization rule for restricted quantification. Note that and needn't be distinct (and illustrates the use of dvelimor 1894). (Contributed by NM, 23-Nov-1994.) (Proof rewritten by Jim Kingdon, 1-Jun-2018.)

Theoremrgenw 2376 Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)

Theoremrgen2w 2377 Generalization rule for restricted quantification. Note that and needn't be distinct. (Contributed by NM, 18-Jun-2014.)

Theoremmprg 2378 Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.)

Theoremmprgbir 2379 Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)

Theoremralim 2380 Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.)

Theoremralimi2 2381 Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.)

Theoremralimia 2382 Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)

Theoremralimiaa 2383 Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.)

Theoremralimi 2384 Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)

Theoremral2imi 2385 Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.)

Theoremralimdaa 2386 Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-Sep-2003.)

Theoremralimdva 2387* Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)

Theoremralimdv 2388* Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 8-Oct-2003.)

Theoremralimdv2 2389* Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.)

Theoremralrimi 2390 Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.)

Theoremralrimiv 2391* Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.)

Theoremralrimiva 2392* Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)

Theoremralrimivw 2393* Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)

Theoremr19.21t 2394 Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers (closed theorem version). (Contributed by NM, 1-Mar-2008.)

Theoremr19.21 2395 Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers. (Contributed by Scott Fenton, 30-Mar-2011.)

Theoremr19.21v 2396* 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 2397 Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 16-Feb-2004.)

Theoremralrimdv 2398* Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 27-May-1998.)

Theoremralrimdva 2399* Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.)

Theoremralrimivv 2400* Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.)

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-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10124
 Copyright terms: Public domain < Previous  Next >