Home | Intuitionistic Logic Explorer Theorem List (p. 22 of 106) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | syl5req 2101 | An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
Theorem | syl5eqr 2102 | An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |
Theorem | syl5reqr 2103 | An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
Theorem | syl6eq 2104 | An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |
Theorem | syl6req 2105 | An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
Theorem | syl6eqr 2106 | An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |
Theorem | syl6reqr 2107 | An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
Theorem | sylan9eq 2108 | An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Theorem | sylan9req 2109 | An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.) |
Theorem | sylan9eqr 2110 | An equality transitivity deduction. (Contributed by NM, 8-May-1994.) |
Theorem | 3eqtr3g 2111 | A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.) |
Theorem | 3eqtr3a 2112 | A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.) |
Theorem | 3eqtr4g 2113 | A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.) |
Theorem | 3eqtr4a 2114 | 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 2115 | A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004.) |
Theorem | eleq1 2116 | Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.) |
Theorem | eleq2 2117 | Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.) |
Theorem | eleq12 2118 | Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.) |
Theorem | eleq1i 2119 | Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.) |
Theorem | eleq2i 2120 | Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.) |
Theorem | eleq12i 2121 | Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.) |
Theorem | eleq1d 2122 | Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.) |
Theorem | eleq2d 2123 | Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.) |
Theorem | eleq12d 2124 | Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.) |
Theorem | eleq1a 2125 | A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.) |
Theorem | eqeltri 2126 | Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |
Theorem | eqeltrri 2127 | Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |
Theorem | eleqtri 2128 | Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |
Theorem | eleqtrri 2129 | Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |
Theorem | eqeltrd 2130 | Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.) |
Theorem | eqeltrrd 2131 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
Theorem | eleqtrd 2132 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
Theorem | eleqtrrd 2133 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
Theorem | 3eltr3i 2134 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
Theorem | 3eltr4i 2135 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
Theorem | 3eltr3d 2136 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
Theorem | 3eltr4d 2137 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
Theorem | 3eltr3g 2138 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
Theorem | 3eltr4g 2139 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
Theorem | syl5eqel 2140 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Theorem | syl5eqelr 2141 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Theorem | syl5eleq 2142 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Theorem | syl5eleqr 2143 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Theorem | syl6eqel 2144 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Theorem | syl6eqelr 2145 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Theorem | syl6eleq 2146 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Theorem | syl6eleqr 2147 | A membership and equality inference. (Contributed by NM, 24-Apr-2005.) |
Theorem | eleq2s 2148 | Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Theorem | eqneltrd 2149 | 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 2150 | 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 2151 | 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 2152 | 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 2153* | Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqf 2217. (Contributed by NM, 5-Aug-1993.) |
Theorem | nelneq 2154 | A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997.) |
Theorem | nelneq2 2155 | A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002.) |
Theorem | eqsb3lem 2156* | Lemma for eqsb3 2157. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Theorem | eqsb3 2157* | Substitution applied to an atomic wff (class version of equsb3 1841). (Contributed by Rodolfo Medina, 28-Apr-2010.) |
Theorem | clelsb3 2158* | Substitution applied to an atomic wff (class version of elsb3 1868). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Theorem | clelsb4 2159* | Substitution applied to an atomic wff (class version of elsb4 1869). (Contributed by Jim Kingdon, 22-Nov-2018.) |
Theorem | hbxfreq 2160 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1377 for equivalence version. (Contributed by NM, 21-Aug-2007.) |
Theorem | hblem 2161* | Change the free variable of a hypothesis builder. (Contributed by NM, 5-Aug-1993.) (Revised by Andrew Salmon, 11-Jul-2011.) |
Theorem | abeq2 2162* |
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 2167 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 2163* | Equality of a class variable and a class abstraction. (Contributed by NM, 20-Aug-1993.) |
Theorem | abeq2i 2164 | Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 3-Apr-1996.) |
Theorem | abeq1i 2165 | Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 31-Jul-1994.) |
Theorem | abeq2d 2166 | Equality of a class variable and a class abstraction (deduction). (Contributed by NM, 16-Nov-1995.) |
Theorem | abbi 2167 | Equivalent wff's correspond to equal class abstractions. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) |
Theorem | abbi2i 2168* | Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 5-Aug-1993.) |
Theorem | abbii 2169 | Equivalent wff's yield equal class abstractions (inference rule). (Contributed by NM, 5-Aug-1993.) |
Theorem | abbid 2170 | Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Theorem | abbidv 2171* | Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 10-Aug-1993.) |
Theorem | abbi2dv 2172* | Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) |
Theorem | abbi1dv 2173* | Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) |
Theorem | abid2 2174* | A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.) |
Theorem | sb8ab 2175 | Substitution of variable in class abstraction. (Contributed by Jim Kingdon, 27-Sep-2018.) |
Theorem | cbvab 2176 | Rule used to change bound variables, using implicit substitution. (Contributed by Andrew Salmon, 11-Jul-2011.) |
Theorem | cbvabv 2177* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.) |
Theorem | clelab 2178* | Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993.) |
Theorem | clabel 2179* | Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006.) |
Theorem | sbab 2180* | 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.) |
Syntax | wnfc 2181 | Extend wff definition to include the not-free predicate for classes. |
Theorem | nfcjust 2182* | Justification theorem for df-nfc 2183. (Contributed by Mario Carneiro, 13-Oct-2016.) |
Definition | df-nfc 2183* | 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 1366 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfci 2184* | Deduce that a class does not have free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfcii 2185* | Deduce that a class does not have free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfcr 2186* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfcrii 2187* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfcri 2188* | Consequence of the not-free predicate. (Note that unlike nfcr 2186, this does not require and to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfcd 2189* | Deduce that a class does not have free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfceqi 2190 | Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfcxfr 2191 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfcxfrd 2192 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfceqdf 2193 | An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016.) |
Theorem | nfcv 2194* | If is disjoint from , then is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfcvd 2195* | If is disjoint from , then is not free in . (Contributed by Mario Carneiro, 7-Oct-2016.) |
Theorem | nfab1 2196 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfnfc1 2197 | is bound in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfab 2198 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfaba1 2199 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.) |
Theorem | nfnfc 2200 | Hypothesis builder for . (Contributed by Mario Carneiro, 11-Aug-2016.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |