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

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

Theorem List for Intuitionistic Logic Explorer - 1601-1700   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremsb4b 1601 Simplified definition of substitution when variables are distinct. (Contributed by NM, 27-May-1997.)
 
Theoremsb4bor 1602 Simplified definition of substitution when variables are distinct, expressed via disjunction. (Contributed by Jim Kingdon, 18-Mar-2018.)
 
Theoremhbsb2 1603 Bound-variable hypothesis builder for substitution. (Contributed by NM, 5-Aug-1993.)
 
Theoremnfsb2or 1604 Bound-variable hypothesis builder for substitution. Similar to hbsb2 1603 but in intuitionistic logic a disjunction is stronger than an implication. (Contributed by Jim Kingdon, 2-Feb-2018.)
 F/
 
Theoremsbequilem 1605 Propositional logic lemma used in the sbequi 1606 proof. (Contributed by Jim Kingdon, 1-Feb-2018.)
   &       =>   
 
Theoremsbequi 1606 An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.) (Proof modified by Jim Kingdon, 1-Feb-2018.)
 
Theoremsbequ 1607 An equality theorem for substitution. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 5-Aug-1993.)
 
Theoremdrsb2 1608 Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 27-Feb-2005.)
 
Theorema4sbe 1609 A specialization theorem, mostly the same as Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 29-Dec-2017.)
 
Theorema4sbim 1610 Specialization of implication. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 21-Jan-2018.)
 
Theorema4sbbi 1611 Specialization of biconditional. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 21-Jan-2018.)
 
Theoremsbbid 1612 Deduction substituting both sides of a biconditional. (Contributed by NM, 5-Aug-1993.)
   &       =>   
 
Theoremsbequ8 1613 Elimination of equality from antecedent after substitution. (Contributed by NM, 5-Aug-1993.) (Proof revised by Jim Kingdon, 20-Jan-2018.)
 
Theoremsbf3t 1614 Substitution has no effect on a non-free variable. (Contributed by NM, 30-May-2009.)
 
Theoremsbid2 1615 An identity law for substitution. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremsbidm 1616 An idempotent law for substitution. (Contributed by NM, 30-Jun-1994.) (Proof rewritten by Jim Kingdon, 21-Jan-2018.)
 
Theoremsb5rf 1617 Reversed substitution. (Contributed by NM, 3-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   =>   
 
Theoremsb6rf 1618 Reversed substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   =>   
 
Theoremsb8 1619 Substitution of variable in universal quantifier. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Jim Kingdon, 15-Jan-2018.)
   =>   
 
Theoremsb8e 1620 Substitution of variable in existential quantifier. (Contributed by NM, 12-Aug-1993.) (Proof rewritten by Jim Kingdon, 15-Jan-2018.)
   =>   
 
1.4.4  Predicate calculus with distinct variables (cont.)
 
Theoremax16i 1621* Inference with ax-16 1581 as its conclusion, that doesn't require ax-10 1329, ax-11 1330, or ax-12 1335 for its proof. The hypotheses may be eliminable without one or more of these axioms in special cases. (Contributed by NM, 20-May-2008.)
   &       =>   
 
Theoremax16ALT 1622* Version of ax16 1580 that doesn't require ax-10 1329 or ax-12 1335 for its proof. (Contributed by NM, 17-May-2008.)
 
Theorema4v 1623* Specialization, using implicit substitition. (Contributed by NM, 30-Aug-1993.)
   =>   
 
Theorema4imev 1624* Distinct-variable version of a4ime 1514. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theorema4eiv 1625* Inference from existential specialization, using implicit substitition. (Contributed by NM, 19-Aug-1993.)
   &       =>   
 
Theoremequvin 1626* A variable introduction law for equality. Lemma 15 of [Monk2] p. 109. (Contributed by NM, 5-Aug-1993.)
 
Theorema16g 1627* A generalization of axiom ax-16 1581. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 
Theorema16gb 1628* A generalization of axiom ax-16 1581. (Contributed by NM, 5-Aug-1993.)
 
Theorema16nf 1629* If there is only one element in the universe, then everything satisfies  F/. (Contributed by Mario Carneiro, 7-Oct-2016.)
 F/
 
Theorem2albidv 1630* Formula-building rule for 2 existential quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.)
   =>   
 
Theorem2exbidv 1631* Formula-building rule for 2 existential quantifiers (deduction rule). (Contributed by NM, 1-May-1995.)
   =>   
 
Theorem3exbidv 1632* Formula-building rule for 3 existential quantifiers (deduction rule). (Contributed by NM, 1-May-1995.)
   =>   
 
Theorem4exbidv 1633* Formula-building rule for 4 existential quantifiers (deduction rule). (Contributed by NM, 3-Aug-1995.)
   =>   
 
Theorem19.9v 1634* Special case of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-May-1995.) (Revised by NM, 21-May-2007.)
 
Theorem19.21v 1635* Special case of Theorem 19.21 of [Margaris] p. 90. Notational convention: We sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as in 19.21 1380 via the use of distinct variable conditions combined with ax-17 1350. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the distinct variable condition; e.g. euf 2081 derived from df-eu 2079. The "f" stands for "not free in" which is less restrictive than "does not occur in." (Contributed by NM, 5-Aug-1993.)
 
Theoremalrimiv 1636* Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremalrimivv 1637* Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
   =>   
 
Theoremalrimdv 1638* Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 10-Feb-1997.)
   =>   
 
Theoremnfdv 1639* Apply the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
   =>     F/
 
Theorem2ax17 1640* Quantification of two variables over a formula in which they do not occur. (Contributed by Alan Sare, 12-Apr-2011.)
 
Theoremalimdv 1641* Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 3-Apr-1994.)
   =>   
 
Theoremeximdv 1642* Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)
   =>   
 
Theorem2alimdv 1643* Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-2004.)
   =>   
 
Theorem2eximdv 1644* Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 3-Aug-1995.)
   =>   
 
Theorem19.23v 1645* Special case of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jun-1998.)
 
Theorem19.23vv 1646* Theorem 19.23 of [Margaris] p. 90 extended to two variables. (Contributed by NM, 10-Aug-2004.)
 
Theoremsb56 1647* Two equivalent ways of expressing the proper substitution of for in , when and are distinct. Theorem 6.2 of [Quine] p. 40. The proof does not involve df-sb 1533. (Contributed by NM, 14-Apr-2008.)
 
Theoremsb6 1648* Equivalence for substitution. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70. (Contributed by NM, 18-Aug-1993.) (Revised by NM, 14-Apr-2008.)
 
Theoremsb5 1649* Equivalence for substitution. Similar to Theorem 6.1 of [Quine] p. 40. (Contributed by NM, 18-Aug-1993.) (Revised by NM, 14-Apr-2008.)
 
Theoremsbnv 1650* Version of sbn 1703 where and are distinct. (Contributed by Jim Kingdon, 18-Dec-2017.)
 
Theoremsbanv 1651* Version of sban 1706 where and are distinct. (Contributed by Jim Kingdon, 24-Dec-2017.)
 
Theoremsborv 1652* Version of sbor 1705 where and are distinct. (Contributed by Jim Kingdon, 3-Feb-2018.)
 
Theoremsbi1v 1653* Forward direction of sbimv 1655. (Contributed by Jim Kingdon, 25-Dec-2017.)
 
Theoremsbi2v 1654* Reverse direction of sbimv 1655. (Contributed by Jim Kingdon, 18-Jan-2018.)
 
Theoremsbimv 1655* Intuitionistic proof of sbim 1704 where and are distinct. (Contributed by Jim Kingdon, 18-Jan-2018.)
 
Theoremsblimv 1656* Version of sblim 1708 where and are distinct. (Contributed by Jim Kingdon, 19-Jan-2018.)
   =>   
 
Theorempm11.53 1657* Theorem *11.53 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
 
Theoremexlimivv 1658* Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 1-Aug-1995.)
   =>   
 
Theoremexlimdvv 1659* Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
   =>   
 
Theorem19.27v 1660* Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 3-Jun-2004.)
 
Theorem19.28v 1661* Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 25-Mar-2004.)
 
Theorem19.36aiv 1662* Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theorem19.41v 1663* Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
 
Theorem19.41vv 1664* Theorem 19.41 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 30-Apr-1995.)
 
Theorem19.41vvv 1665* Theorem 19.41 of [Margaris] p. 90 with 3 quantifiers. (Contributed by NM, 30-Apr-1995.)
 
Theorem19.41vvvv 1666* Theorem 19.41 of [Margaris] p. 90 with 4 quantifiers. (Contributed by FL, 14-Jul-2007.)
 
Theorem19.42v 1667* Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
 
Theoremexdistr 1668* Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.)
 
Theorem19.42vv 1669* Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 16-Mar-1995.)
 
Theorem19.42vvv 1670* Theorem 19.42 of [Margaris] p. 90 with 3 quantifiers. (Contributed by NM, 21-Sep-2011.)
 
Theoremexdistr2 1671* Distribution of existential quantifiers. (Contributed by NM, 17-Mar-1995.)
 
Theorem3exdistr 1672* Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 
Theorem4exdistr 1673* Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.)
 
Theoremcbvalv 1674* Rule used to change bound variables, using implicit substitition. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremcbvexv 1675* Rule used to change bound variables, using implicit substitition. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremcbval2 1676* Rule used to change bound variables, using implicit substitition. (Contributed by NM, 22-Dec-2003.)
   &       &       &       &       =>   
 
Theoremcbvex2 1677* Rule used to change bound variables, using implicit substitition. (Contributed by NM, 14-Sep-2003.)
   &       &       &       &       =>   
 
Theoremcbval2v 1678* Rule used to change bound variables, using implicit substitition. (Contributed by NM, 4-Feb-2005.)
   =>   
 
Theoremcbvex2v 1679* Rule used to change bound variables, using implicit substitition. (Contributed by NM, 26-Jul-1995.)
   =>   
 
Theoremcbvald 1680* Deduction used to change bound variables, using implicit substitition, particularly useful in conjunction with dvelim 1768. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   &       &       =>   
 
Theoremcbvexd 1681* Deduction used to change bound variables, using implicit substitition, particularly useful in conjunction with dvelim 1768. (Contributed by NM, 2-Jan-2002.) (Proof rewritten by Jim Kingdon, 30-Dec-2017.)
   &       &       =>   
 
Theoremcbvex4v 1682* Rule used to change bound variables, using implicit substitition. (Contributed by NM, 26-Jul-1995.)
   &       =>   
 
Theoremeean 1683 Rearrange existential quantifiers. (Contributed by NM, 27-Oct-2010.)
   &       =>   
 
Theoremeeanv 1684* Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)
 
Theoremeeeanv 1685* Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 
Theoremee4anv 1686* Rearrange existential quantifiers. (Contributed by NM, 31-Jul-1995.)
 
Theoremnexdv 1687* Deduction for generalization rule for negated wff. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremchvarv 1688* Implicit substitution of for into a theorem. (Contributed by NM, 20-Apr-1994.)
   &       =>   
 
Theoremcleljust 1689* When the class variables of set theory are replaced with set variables, this theorem of predicate calculus is the result. This theorem provides part of the justification for the consistency of that definition, which "overloads" the set variables in wel 1327 with the class variables in wcel 1326. (Contributed by NM, 28-Jan-2004.)
 
1.4.5  More substitution theorems
 
Theoremhbs1 1690* is not free in when and are distinct. (Contributed by NM, 5-Aug-1993.) (Proof by Jim Kingdon, 16-Dec-2017.)
 
Theoremnfs1v 1691* is not free in when and are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)

 F/
 
Theoremsbhb 1692* Two ways of expressing " is (effectively) not free in ." (Contributed by NM, 29-May-2009.)
 
Theoremsbhb2 1693* Two ways of expressing " is (effectively) not free in ." (Contributed by Gérard Lang, 14-Nov-2013.)
 
Theoremhbsbv 1694* This is a version of hbsb 1700 with an extra distinct variable constraint, on and . (Contributed by Jim Kingdon, 25-Dec-2017.)
   =>   
 
Theoremnfsbxy 1695* Similar to hbsb 1700 but with an extra distinct variable constraint, on and . (Contributed by Jim Kingdon, 19-Mar-2018.)

 F/   =>    
 F/
 
Theoremnfsbxyt 1696* Closed form of nfsbxy 1695. (Contributed by Jim Kingdon, 9-May-2018.)
 F/  F/
 
Theoremsbco2vlem 1697* This is a version of sbco2 1716 where is distinct from and from . It is a lemma on the way to proving sbco2v 1698 which only requires that and be distinct. (Contributed by Jim Kingdon, 25-Dec-2017.) (One distinct variable constraint removed by Jim Kingdon, 3-Feb-2018.)
   =>   
 
Theoremsbco2v 1698* This is a version of sbco2 1716 where is distinct from . (Contributed by Jim Kingdon, 12-Feb-2018.)
   =>   
 
Theoremnfsb 1699* If is not free in , it is not free in when and are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof rewritten by Jim Kingdon, 19-Mar-2018.)

 F/   =>    
 F/
 
Theoremhbsb 1700* If is not free in , it is not free in when and are distinct. (Contributed by NM, 12-Aug-1993.) (Proof rewritten by Jim Kingdon, 22-Mar-2018.)
   =>   
    < 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-2186
  Copyright terms: Public domain < Previous  Next >