Home | Intuitionistic Logic ExplorerTheorem List (p. 19 of 21)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | eqeq2d 1801 | Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.) |

Theorem | eqeq12 1802 | Equality relationship among 4 classes. (Contributed by NM, 3-Aug-1994.) |

Theorem | eqeq12i 1803 | A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |

Theorem | eqeq12d 1804 | A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |

Theorem | eqeqan12d 1805 | A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) |

Theorem | eqeqan12rd 1806 | A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.) |

Theorem | eqtr 1807 | Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.) |

Theorem | eqtr2 1808 | A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) |

Theorem | eqtr3 1809 | A transitive law for class equality. (Contributed by NM, 20-May-2005.) |

Theorem | eqtri 1810 | An equality transitivity inference. (Contributed by NM, 5-Aug-1993.) |

Theorem | eqtr2i 1811 | An equality transitivity inference. (Contributed by NM, 21-Feb-1995.) |

Theorem | eqtr3i 1812 | An equality transitivity inference. (Contributed by NM, 6-May-1994.) |

Theorem | eqtr4i 1813 | An equality transitivity inference. (Contributed by NM, 5-Aug-1993.) |

Theorem | 3eqtri 1814 | An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.) |

Theorem | 3eqtrri 1815 | An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) |

Theorem | 3eqtr2i 1816 | An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) |

Theorem | 3eqtr2ri 1817 | An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) |

Theorem | 3eqtr3i 1818 | An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) |

Theorem | 3eqtr3ri 1819 | An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.) |

Theorem | 3eqtr4i 1820 | An inference from three chained equalities. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |

Theorem | 3eqtr4ri 1821 | An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) |

Theorem | eqtrd 1822 | An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |

Theorem | eqtr2d 1823 | An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.) |

Theorem | eqtr3d 1824 | An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.) |

Theorem | eqtr4d 1825 | An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.) |

Theorem | 3eqtrd 1826 | A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.) |

Theorem | 3eqtrrd 1827 | A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) |

Theorem | 3eqtr2d 1828 | A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) |

Theorem | 3eqtr2rd 1829 | A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) |

Theorem | 3eqtr3d 1830 | A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) |

Theorem | 3eqtr3rd 1831 | A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.) |

Theorem | 3eqtr4d 1832 | A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) |

Theorem | 3eqtr4rd 1833 | A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.) |

Theorem | syl5eq 1834 | An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |

Theorem | syl5req 1835 | An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |

Theorem | syl5eqr 1836 | An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |

Theorem | syl5reqr 1837 | An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |

Theorem | syl6eq 1838 | An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |

Theorem | syl6req 1839 | An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |

Theorem | syl6eqr 1840 | An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |

Theorem | syl6reqr 1841 | An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |

Theorem | sylan9eq 1842 | An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) |

Theorem | sylan9req 1843 | An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.) |

Theorem | sylan9eqr 1844 | An equality transitivity deduction. (Contributed by NM, 8-May-1994.) |

Theorem | 3eqtr3g 1845 | A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.) |

Theorem | 3eqtr3a 1846 | A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.) |

Theorem | 3eqtr4g 1847 | A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.) |

Theorem | 3eqtr4a 1848 | A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |

Theorem | eq2tri 1849 | A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004.) |

Theorem | eleq1 1850 | Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.) |

Theorem | eleq2 1851 | Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.) |

Theorem | eleq12 1852 | Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.) |

Theorem | eleq1i 1853 | Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.) |

Theorem | eleq2i 1854 | Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.) |

Theorem | eleq12i 1855 | Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.) |

Theorem | eleq1d 1856 | Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.) |

Theorem | eleq2d 1857 | Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.) |

Theorem | eleq12d 1858 | Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.) |

Theorem | eleq1a 1859 | A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.) |

Theorem | eqeltri 1860 | Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |

Theorem | eqeltrri 1861 | Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |

Theorem | eleqtri 1862 | Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |

Theorem | eleqtrri 1863 | Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |

Theorem | eqeltrd 1864 | Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.) |

Theorem | eqeltrrd 1865 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |

Theorem | eleqtrd 1866 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |

Theorem | eleqtrrd 1867 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |

Theorem | 3eltr3i 1868 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |

Theorem | 3eltr4i 1869 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |

Theorem | 3eltr3d 1870 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |

Theorem | 3eltr4d 1871 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |

Theorem | 3eltr3g 1872 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |

Theorem | 3eltr4g 1873 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |

Theorem | syl5eqel 1874 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |

Theorem | syl5eqelr 1875 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |

Theorem | syl5eleq 1876 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |

Theorem | syl5eleqr 1877 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |

Theorem | syl6eqel 1878 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |

Theorem | syl6eqelr 1879 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |

Theorem | syl6eleq 1880 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |

Theorem | syl6eleqr 1881 | A membership and equality inference. (Contributed by NM, 24-Apr-2005.) |

Theorem | eleq2s 1882 | Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |

Theorem | eqneltrd 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.) |

Theorem | eqneltrrd 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.) |

Theorem | neleqtrd 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.) |

Theorem | neleqtrrd 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.) |

Theorem | cleqh 1887* | Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 5-Aug-1993.) |

Theorem | nelneq 1888 | A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997.) |

Theorem | nelneq2 1889 | A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002.) |

Theorem | eqsb3lem 1890* | Lemma for eqsb3 1891. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |

Theorem | eqsb3 1891* | Substitution applied to an atomic wff (class version of equsb3 1700). (Contributed by Rodolfo Medina, 28-Apr-2010.) |

Theorem | clelsb3 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.) |

Theorem | hbxfreq 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.) |

Theorem | hblem 1894* | Change the free variable of a hypothesis builder. (Contributed by NM, 5-Aug-1993.) (Revised by Andrew Salmon, 11-Jul-2011.) |

Theorem | abeq2 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.) |

Theorem | abeq1 1896* | Equality of a class variable and a class abstraction. (Contributed by NM, 20-Aug-1993.) |

Theorem | abeq2i 1897 | Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 3-Apr-1996.) |

Theorem | abeq1i 1898 | Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 31-Jul-1994.) |

Theorem | abeq2d 1899 | Equality of a class variable and a class abstraction (deduction). (Contributed by NM, 16-Nov-1995.) |

Theorem | abbi 1900 | Equivalent wff's correspond to equal class abstractions. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |