HomeHome Intuitionistic Logic Explorer
Theorem List (p. 19 of 21)
< 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 - 1801-1900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremeqeq2d 1801 Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
   =>     C  C
 
Theoremeqeq12 1802 Equality relationship among 4 classes. (Contributed by NM, 3-Aug-1994.)
 C  D  C  D
 
Theoremeqeq12i 1803 A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   &     C  D   =>     C  D
 
Theoremeqeq12d 1804 A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   &     C  D   =>     C  D
 
Theoremeqeqan12d 1805 A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   &     C  D   =>     C  D
 
Theoremeqeqan12rd 1806 A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.)
   &     C  D   =>     C  D
 
Theoremeqtr 1807 Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.)
 C  C
 
Theoremeqtr2 1808 A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 C  C
 
Theoremeqtr3 1809 A transitive law for class equality. (Contributed by NM, 20-May-2005.)
 C  C
 
Theoremeqtri 1810 An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
   &     C   =>     C
 
Theoremeqtr2i 1811 An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
   &     C   =>     C
 
Theoremeqtr3i 1812 An equality transitivity inference. (Contributed by NM, 6-May-1994.)
   &     C   =>     C
 
Theoremeqtr4i 1813 An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
   &     C    =>     C
 
Theorem3eqtri 1814 An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
   &     C   &     C  D   =>     D
 
Theorem3eqtrri 1815 An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   &     C   &     C  D   =>     D
 
Theorem3eqtr2i 1816 An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)
   &     C    &     C  D   =>     D
 
Theorem3eqtr2ri 1817 An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   &     C    &     C  D   =>     D
 
Theorem3eqtr3i 1818 An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   &     C   &     D   =>     C  D
 
Theorem3eqtr3ri 1819 An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
   &     C   &     D   =>     D  C
 
Theorem3eqtr4i 1820 An inference from three chained equalities. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   &     C    &     D    =>     C  D
 
Theorem3eqtr4ri 1821 An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   &     C    &     D    =>     D  C
 
Theoremeqtrd 1822 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
   &     C   =>     C
 
Theoremeqtr2d 1823 An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
   &     C   =>     C
 
Theoremeqtr3d 1824 An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
   &     C   =>     C
 
Theoremeqtr4d 1825 An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
   &     C    =>     C
 
Theorem3eqtrd 1826 A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)
   &     C   &     C  D   =>     D
 
Theorem3eqtrrd 1827 A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   &     C   &     C  D   =>     D
 
Theorem3eqtr2d 1828 A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
   &     C    &     C  D   =>     D
 
Theorem3eqtr2rd 1829 A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
   &     C    &     C  D   =>     D
 
Theorem3eqtr3d 1830 A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   &     C   &     D   =>     C  D
 
Theorem3eqtr3rd 1831 A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
   &     C   &     D   =>     D  C
 
Theorem3eqtr4d 1832 A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   &     C    &     D    =>     C  D
 
Theorem3eqtr4rd 1833 A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
   &     C    &     D    =>     D  C
 
Theoremsyl5eq 1834 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
   &     C   =>     C
 
Theoremsyl5req 1835 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
   &     C   =>     C
 
Theoremsyl5eqr 1836 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
   &     C   =>     C
 
Theoremsyl5reqr 1837 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
   &     C   =>     C
 
Theoremsyl6eq 1838 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
   &     C   =>     C
 
Theoremsyl6req 1839 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
   &     C   =>     C
 
Theoremsyl6eqr 1840 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
   &     C    =>     C
 
Theoremsyl6reqr 1841 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
   &     C    =>     C
 
Theoremsylan9eq 1842 An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   &     C   =>     C
 
Theoremsylan9req 1843 An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
   &     C   =>     C
 
Theoremsylan9eqr 1844 An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
   &     C   =>     C
 
Theorem3eqtr3g 1845 A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)
   &     C   &     D   =>     C  D
 
Theorem3eqtr3a 1846 A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)
   &     C   &     D   =>     C  D
 
Theorem3eqtr4g 1847 A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.)
   &     C    &     D    =>     C  D
 
Theorem3eqtr4a 1848 A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   &     C    &     D    =>     C  D
 
Theoremeq2tri 1849 A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004.)
 C  D  F   &     D  C  G   =>     C  F  D  G
 
Theoremeleq1 1850 Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
 C  C
 
Theoremeleq2 1851 Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
 C  C
 
Theoremeleq12 1852 Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)
 C  D  C  D
 
Theoremeleq1i 1853 Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
   =>     C  C
 
Theoremeleq2i 1854 Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
   =>     C  C
 
Theoremeleq12i 1855 Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
   &     C  D   =>     C  D
 
Theoremeleq1d 1856 Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
   =>     C  C
 
Theoremeleq2d 1857 Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)
   =>     C  C
 
Theoremeleq12d 1858 Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
   &     C  D   =>     C  D
 
Theoremeleq1a 1859 A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
 C  C
 
Theoremeqeltri 1860 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
   &     C   =>     C
 
Theoremeqeltrri 1861 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
   &     C   =>     C
 
Theoremeleqtri 1862 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
   &     C   =>     C
 
Theoremeleqtrri 1863 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
   &     C    =>     C
 
Theoremeqeltrd 1864 Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)
   &     C   =>     C
 
Theoremeqeltrrd 1865 Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
   &     C   =>     C
 
Theoremeleqtrd 1866 Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
   &     C   =>     C
 
Theoremeleqtrrd 1867 Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
   &     C    =>     C
 
Theorem3eltr3i 1868 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
   &     C   &     D   =>     C  D
 
Theorem3eltr4i 1869 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
   &     C    &     D    =>     C  D
 
Theorem3eltr3d 1870 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
   &     C   &     D   =>     C  D
 
Theorem3eltr4d 1871 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
   &     C    &     D    =>     C  D
 
Theorem3eltr3g 1872 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
   &     C   &     D   =>     C  D
 
Theorem3eltr4g 1873 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
   &     C    &     D    =>     C  D
 
Theoremsyl5eqel 1874 B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
   &     C   =>     C
 
Theoremsyl5eqelr 1875 B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
   &     C   =>     C
 
Theoremsyl5eleq 1876 B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
   &     C   =>     C
 
Theoremsyl5eleqr 1877 B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
   &     C    =>     C
 
Theoremsyl6eqel 1878 A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
   &     C   =>     C
 
Theoremsyl6eqelr 1879 A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
   &     C   =>     C
 
Theoremsyl6eleq 1880 A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
   &     C   =>     C
 
Theoremsyl6eleqr 1881 A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
   &     C    =>     C
 
Theoremeleq2s 1882 Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
   &     C    =>     C
 
Theoremeqneltrd 1883 If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.)
   &     C   =>     C
 
Theoremeqneltrrd 1884 If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.)
   &     C   =>     C
 
Theoremneleqtrd 1885 If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.)
 C    &       =>     C
 
Theoremneleqtrrd 1886 If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.)
 C    &       =>     C
 
Theoremcleqh 1887* Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 5-Aug-1993.)
   &       =>   
 
Theoremnelneq 1888 A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997.)
 C  C
 
Theoremnelneq2 1889 A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002.)
 C  C
 
Theoremeqsb3lem 1890* Lemma for eqsb3 1891. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
 
Theoremeqsb3 1891* Substitution applied to an atomic wff (class version of equsb3 1700). (Contributed by Rodolfo Medina, 28-Apr-2010.)
 
Theoremclelsb3 1892* Substitution applied to an atomic wff (class version of elsb3 1727). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
 
Theoremhbxfreq 1893 A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1290 for equivalence version. (Contributed by NM, 21-Aug-2007.)
   &       =>   
 
Theoremhblem 1894* Change the free variable of a hypothesis builder. (Contributed by NM, 5-Aug-1993.) (Revised by Andrew Salmon, 11-Jul-2011.)
   =>   
 
Theoremabeq2 1895* Equality of a class variable and a class abstraction (also called a class builder). Theorem 5.1 of [Quine] p. 34. This theorem shows the relationship between expressions with class abstractions and expressions with class variables. Note that abbi 1900 and its relatives are among those useful for converting theorems with class variables to equivalent theorems with wff variables, by first substituting a class abstraction for each class variable.

Class variables can always be eliminated from a theorem to result in an equivalent theorem with wff variables, and vice-versa. The idea is roughly as follows. To convert a theorem with a wff variable (that has a free variable ) to a theorem with a class variable , we substitute for throughout and simplify, where is a new class variable not already in the wff. Conversely, to convert a theorem with a class variable to one with , we substitute  {  |  } for throughout and simplify, where and are new set and wff variables not already in the wff. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. (Contributed by NM, 5-Aug-1993.)

 {  |  }
 
Theoremabeq1 1896* Equality of a class variable and a class abstraction. (Contributed by NM, 20-Aug-1993.)
 {  | 
 }
 
Theoremabeq2i 1897 Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 3-Apr-1996.)
 {  |  }   =>   
 
Theoremabeq1i 1898 Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 31-Jul-1994.)

 {  |  }    =>   
 
Theoremabeq2d 1899 Equality of a class variable and a class abstraction (deduction). (Contributed by NM, 16-Nov-1995.)
 {  |  }   =>   
 
Theoremabbi 1900 Equivalent wff's correspond to equal class abstractions. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.)
 {  |  }  {  |  }
    < 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-2099
  Copyright terms: Public domain < Previous  Next >