Home | Intuitionistic Logic ExplorerTheorem List (p. 20 of 25)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

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

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

Statement | ||

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

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

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

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

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

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

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

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

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

Theorem | 3eqtr4a 1910 | 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 1911 | A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004.) |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem | eqneltrd 1945 | 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 1946 | 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 1947 | 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 1948 | 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 1949* | Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 5-Aug-1993.) |

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

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

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

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

Theorem | clelsb3 1954* | Substitution applied to an atomic wff (class version of elsb3 1751). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |

Theorem | hbxfreq 1955 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1293 for equivalence version. (Contributed by NM, 21-Aug-2007.) |

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

Theorem | abeq2 1957* |
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 1962 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 1958* | Equality of a class variable and a class abstraction. (Contributed by NM, 20-Aug-1993.) |

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

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

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

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

Theorem | abbi2i 1963* | Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 5-Aug-1993.) |

Theorem | abbii 1964 | Equivalent wff's yield equal class abstractions (inference rule). (Contributed by NM, 5-Aug-1993.) |

Theorem | abbid 1965 | Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) |

Theorem | abbidv 1966* | Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 10-Aug-1993.) |

Theorem | abbi2dv 1967* | Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) |

Theorem | abbi1dv 1968* | Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) |

Theorem | abid2 1969* | A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.) |

Theorem | cbvab 1970 | Rule used to change bound variables, using implicit substitution. (Contributed by Andrew Salmon, 11-Jul-2011.) |

Theorem | cbvabv 1971* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.) |

Theorem | clelab 1972* | Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993.) |

Theorem | clabel 1973* | Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006.) |

Theorem | sbab 1974* | The right-hand side of the second equality is a way of representing proper substitution of for into a class variable. (Contributed by NM, 14-Sep-2003.) |

2.1.3 Class form not-free predicate | ||

Syntax | wnfc 1975 | Extend wff definition to include the not-free predicate for classes. |

Theorem | nfcjust 1976* | Justification theorem for df-nfc 1977. (Contributed by Mario Carneiro, 13-Oct-2016.) |

Definition | df-nfc 1977* | Define the not-free predicate for classes. This is read " is not free in ". Not-free means that the value of cannot affect the value of , e.g., any occurrence of in is effectively bound by a quantifier or something that expands to one (such as "there exists at most one"). It is defined in terms of the not-free predicate df-nf 1282 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfci 1978* | Deduce that a class does not have free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfcii 1979* | Deduce that a class does not have free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfcr 1980* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfcrii 1981* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfcri 1982* | Consequence of the not-free predicate. (Note that unlike nfcr 1980, this does not require and to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfcd 1983* | Deduce that a class does not have free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfceqi 1984 | Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfcxfr 1985 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfcxfrd 1986 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfceqdf 1987 | An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016.) |

Theorem | nfcv 1988* | If is disjoint from , then is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfcvd 1989* | If is disjoint from , then is not free in . (Contributed by Mario Carneiro, 7-Oct-2016.) |

Theorem | nfab1 1990 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfnfc1 1991 | is bound in . (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfab 1992 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfaba1 1993 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.) |

Theorem | nfnfc 1994 | Hypothesis builder for . (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfeq 1995 | Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfel 1996 | Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfeq1 1997* | Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |

Theorem | nfel1 1998* | Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |

Theorem | nfeq2 1999* | Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |

Theorem | nfel2 2000* | Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |