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