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