Home | Intuitionistic Logic Explorer Theorem List (p. 23 of 130) | < 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 | syl5eleq 2201 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Theorem | syl5eleqr 2202 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Theorem | syl6eqel 2203 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Theorem | syl6eqelr 2204 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Theorem | syl6eleq 2205 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Theorem | syl6eleqr 2206 | A membership and equality inference. (Contributed by NM, 24-Apr-2005.) |
Theorem | eleq2s 2207 | Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Theorem | eqneltrd 2208 | 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 2209 | 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 2210 | 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 2211 | 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 2212* | Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqf 2277. (Contributed by NM, 5-Aug-1993.) |
Theorem | nelneq 2213 | A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997.) |
Theorem | nelneq2 2214 | A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002.) |
Theorem | eqsb3lem 2215* | Lemma for eqsb3 2216. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Theorem | eqsb3 2216* | Substitution applied to an atomic wff (class version of equsb3 1898). (Contributed by Rodolfo Medina, 28-Apr-2010.) |
Theorem | clelsb3 2217* | Substitution applied to an atomic wff (class version of elsb3 1925). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Theorem | clelsb4 2218* | Substitution applied to an atomic wff (class version of elsb4 1926). (Contributed by Jim Kingdon, 22-Nov-2018.) |
Theorem | hbxfreq 2219 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1429 for equivalence version. (Contributed by NM, 21-Aug-2007.) |
Theorem | hblem 2220* | Change the free variable of a hypothesis builder. (Contributed by NM, 5-Aug-1993.) (Revised by Andrew Salmon, 11-Jul-2011.) |
Theorem | abeq2 2221* |
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 2226 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 2222* | Equality of a class variable and a class abstraction. (Contributed by NM, 20-Aug-1993.) |
Theorem | abeq2i 2223 | Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.) |
Theorem | abeq1i 2224 | Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 31-Jul-1994.) |
Theorem | abeq2d 2225 | Equality of a class variable and a class abstraction (deduction). (Contributed by NM, 16-Nov-1995.) |
Theorem | abbi 2226 | Equivalent wff's correspond to equal class abstractions. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) |
Theorem | abbi2i 2227* | Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 5-Aug-1993.) |
Theorem | abbii 2228 | Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 5-Aug-1993.) |
Theorem | abbid 2229 | Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Theorem | abbidv 2230* | Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.) |
Theorem | abbi2dv 2231* | Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) |
Theorem | abbi1dv 2232* | Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) |
Theorem | abid2 2233* | A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.) |
Theorem | sb8ab 2234 | Substitution of variable in class abstraction. (Contributed by Jim Kingdon, 27-Sep-2018.) |
Theorem | cbvab 2235 | Rule used to change bound variables, using implicit substitution. (Contributed by Andrew Salmon, 11-Jul-2011.) |
Theorem | cbvabv 2236* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.) |
Theorem | clelab 2237* | Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993.) |
Theorem | clabel 2238* | Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006.) |
Theorem | sbab 2239* | 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 2240 | Extend wff definition to include the not-free predicate for classes. |
Theorem | nfcjust 2241* | Justification theorem for df-nfc 2242. (Contributed by Mario Carneiro, 13-Oct-2016.) |
Definition | df-nfc 2242* | 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 1418 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfci 2243* | Deduce that a class does not have free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfcii 2244* | Deduce that a class does not have free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfcr 2245* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfcrii 2246* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfcri 2247* | Consequence of the not-free predicate. (Note that unlike nfcr 2245, this does not require and to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfcd 2248* | Deduce that a class does not have free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfceqi 2249 | Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfcxfr 2250 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfcxfrd 2251 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfceqdf 2252 | An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016.) |
Theorem | nfcv 2253* | If is disjoint from , then is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfcvd 2254* | If is disjoint from , then is not free in . (Contributed by Mario Carneiro, 7-Oct-2016.) |
Theorem | nfab1 2255 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfnfc1 2256 | is bound in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | clelsb3f 2257 | Substitution applied to an atomic wff (class version of elsb3 1925). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.) |
Theorem | nfab 2258 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfaba1 2259 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.) |
Theorem | nfnfc 2260 | Hypothesis builder for . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfeq 2261 | Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfel 2262 | Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfeq1 2263* | Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
Theorem | nfel1 2264* | Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
Theorem | nfeq2 2265* | Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
Theorem | nfel2 2266* | Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
Theorem | nfcrd 2267* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfeqd 2268 | Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.) |
Theorem | nfeld 2269 | Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.) |
Theorem | drnfc1 2270 | Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.) |
Theorem | drnfc2 2271 | Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.) |
Theorem | nfabd 2272 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.) |
Theorem | dvelimdc 2273 | Deduction form of dvelimc 2274. (Contributed by Mario Carneiro, 8-Oct-2016.) |
Theorem | dvelimc 2274 | Version of dvelim 1966 for classes. (Contributed by Mario Carneiro, 8-Oct-2016.) |
Theorem | nfcvf 2275 | If and are distinct, then is not free in . (Contributed by Mario Carneiro, 8-Oct-2016.) |
Theorem | nfcvf2 2276 | If and are distinct, then is not free in . (Contributed by Mario Carneiro, 5-Dec-2016.) |
Theorem | cleqf 2277 | Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqh 2212. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Theorem | abid2f 2278 | 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 2279* | 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.) |
Syntax | wne 2280 | Extend wff notation to include inequality. |
Definition | df-ne 2281 | Define inequality. (Contributed by NM, 5-Aug-1993.) |
Theorem | neii 2282 | Inference associated with df-ne 2281. (Contributed by BJ, 7-Jul-2018.) |
Theorem | neir 2283 | Inference associated with df-ne 2281. (Contributed by BJ, 7-Jul-2018.) |
Theorem | nner 2284 | Negation of inequality. (Contributed by Jim Kingdon, 23-Dec-2018.) |
Theorem | nnedc 2285 | Negation of inequality where equality is decidable. (Contributed by Jim Kingdon, 15-May-2018.) |
DECID | ||
Theorem | dcned 2286 | Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.) |
DECID DECID | ||
Theorem | neqned 2287 | If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2301. One-way deduction form of df-ne 2281. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2330. (Revised by Wolf Lammen, 22-Nov-2019.) |
Theorem | neqne 2288 | From non-equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | neirr 2289 | No class is unequal to itself. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Proof rewritten by Jim Kingdon, 15-May-2018.) |
Theorem | eqneqall 2290 | A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.) |
Theorem | dcne 2291 | Decidable equality expressed in terms of . Basically the same as df-dc 803. (Contributed by Jim Kingdon, 14-Mar-2020.) |
DECID | ||
Theorem | nonconne 2292 | Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.) |
Theorem | neeq1 2293 | Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) |
Theorem | neeq2 2294 | Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) |
Theorem | neeq1i 2295 | Inference for inequality. (Contributed by NM, 29-Apr-2005.) |
Theorem | neeq2i 2296 | Inference for inequality. (Contributed by NM, 29-Apr-2005.) |
Theorem | neeq12i 2297 | Inference for inequality. (Contributed by NM, 24-Jul-2012.) |
Theorem | neeq1d 2298 | Deduction for inequality. (Contributed by NM, 25-Oct-1999.) |
Theorem | neeq2d 2299 | Deduction for inequality. (Contributed by NM, 25-Oct-1999.) |
Theorem | neeq12d 2300 | Deduction for inequality. (Contributed by NM, 24-Jul-2012.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |