Home | Intuitionistic Logic Explorer Theorem List (p. 34 of 115) | < 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 | rabeq0 3301 | Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.) |
Theorem | abeq0 3302 | Condition for a class abstraction to be empty. (Contributed by Jim Kingdon, 12-Aug-2018.) |
Theorem | rabxmdc 3303* | Law of excluded middle given decidability, in terms of restricted class abstractions. (Contributed by Jim Kingdon, 2-Aug-2018.) |
DECID | ||
Theorem | rabnc 3304* | Law of noncontradiction, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) |
Theorem | un0 3305 | The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.) |
Theorem | in0 3306 | The intersection of a class with the empty set is the empty set. Theorem 16 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.) |
Theorem | inv1 3307 | The intersection of a class with the universal class is itself. Exercise 4.10(k) of [Mendelson] p. 231. (Contributed by NM, 17-May-1998.) |
Theorem | unv 3308 | The union of a class with the universal class is the universal class. Exercise 4.10(l) of [Mendelson] p. 231. (Contributed by NM, 17-May-1998.) |
Theorem | 0ss 3309 | The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.) |
Theorem | ss0b 3310 | Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its converse. (Contributed by NM, 17-Sep-2003.) |
Theorem | ss0 3311 | Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23. (Contributed by NM, 13-Aug-1994.) |
Theorem | sseq0 3312 | A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | ssn0 3313 | A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.) |
Theorem | abf 3314 | A class builder with a false argument is empty. (Contributed by NM, 20-Jan-2012.) |
Theorem | eq0rdv 3315* | Deduction rule for equality to the empty set. (Contributed by NM, 11-Jul-2014.) |
Theorem | csbprc 3316 | The proper substitution of a proper class for a set into a class results in the empty set. (Contributed by NM, 17-Aug-2018.) |
Theorem | un00 3317 | Two classes are empty iff their union is empty. (Contributed by NM, 11-Aug-2004.) |
Theorem | vss 3318 | Only the universal class has the universal class as a subclass. (Contributed by NM, 17-Sep-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | disj 3319* | Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.) |
Theorem | disjr 3320* | Two ways of saying that two classes are disjoint. (Contributed by Jeff Madsen, 19-Jun-2011.) |
Theorem | disj1 3321* | Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 19-Aug-1993.) |
Theorem | reldisj 3322 | Two ways of saying that two classes are disjoint, using the complement of relative to a universe . (Contributed by NM, 15-Feb-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | disj3 3323 | Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998.) |
Theorem | disjne 3324 | Members of disjoint sets are not equal. (Contributed by NM, 28-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | disjel 3325 | A set can't belong to both members of disjoint classes. (Contributed by NM, 28-Feb-2015.) |
Theorem | disj2 3326 | Two ways of saying that two classes are disjoint. (Contributed by NM, 17-May-1998.) |
Theorem | ssdisj 3327 | Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007.) |
Theorem | undisj1 3328 | The union of disjoint classes is disjoint. (Contributed by NM, 26-Sep-2004.) |
Theorem | undisj2 3329 | The union of disjoint classes is disjoint. (Contributed by NM, 13-Sep-2004.) |
Theorem | ssindif0im 3330 | Subclass implies empty intersection with difference from the universal class. (Contributed by NM, 17-Sep-2003.) |
Theorem | inelcm 3331 | The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.) |
Theorem | minel 3332 | A minimum element of a class has no elements in common with the class. (Contributed by NM, 22-Jun-1994.) |
Theorem | undif4 3333 | Distribute union over difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | disjssun 3334 | Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | ssdif0im 3335 | Subclass implies empty difference. One direction of Exercise 7 of [TakeutiZaring] p. 22. In classical logic this would be an equivalence. (Contributed by Jim Kingdon, 2-Aug-2018.) |
Theorem | vdif0im 3336 | Universal class equality in terms of empty difference. (Contributed by Jim Kingdon, 3-Aug-2018.) |
Theorem | difrab0eqim 3337* | If the difference between the restricting class of a restricted class abstraction and the restricted class abstraction is empty, the restricting class is equal to this restricted class abstraction. (Contributed by Jim Kingdon, 3-Aug-2018.) |
Theorem | inssdif0im 3338 | Intersection, subclass, and difference relationship. In classical logic the converse would also hold. (Contributed by Jim Kingdon, 3-Aug-2018.) |
Theorem | difid 3339 | The difference between a class and itself is the empty set. Proposition 5.15 of [TakeutiZaring] p. 20. Also Theorem 32 of [Suppes] p. 28. (Contributed by NM, 22-Apr-2004.) |
Theorem | difidALT 3340 | The difference between a class and itself is the empty set. Proposition 5.15 of [TakeutiZaring] p. 20. Also Theorem 32 of [Suppes] p. 28. Alternate proof of difid 3339. (Contributed by David Abernethy, 17-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | dif0 3341 | The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.) |
Theorem | 0dif 3342 | The difference between the empty set and a class. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.) |
Theorem | disjdif 3343 | A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.) |
Theorem | difin0 3344 | The difference of a class from its intersection is empty. Theorem 37 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | undif1ss 3345 | Absorption of difference by union. In classical logic, as Theorem 35 of [Suppes] p. 29, this would be equality rather than subset. (Contributed by Jim Kingdon, 4-Aug-2018.) |
Theorem | undif2ss 3346 | Absorption of difference by union. In classical logic, as in Part of proof of Corollary 6K of [Enderton] p. 144, this would be equality rather than subset. (Contributed by Jim Kingdon, 4-Aug-2018.) |
Theorem | undifabs 3347 | Absorption of difference by union. (Contributed by NM, 18-Aug-2013.) |
Theorem | inundifss 3348 | The intersection and class difference of a class with another class are contained in the original class. In classical logic we'd be able to make a stronger statement: that everything in the original class is in the intersection or the difference (that is, this theorem would be equality rather than subset). (Contributed by Jim Kingdon, 4-Aug-2018.) |
Theorem | difun2 3349 | Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
Theorem | undifss 3350 | Union of complementary parts into whole. (Contributed by Jim Kingdon, 4-Aug-2018.) |
Theorem | ssdifin0 3351 | A subset of a difference does not intersect the subtrahend. (Contributed by Jeff Hankins, 1-Sep-2013.) (Proof shortened by Mario Carneiro, 24-Aug-2015.) |
Theorem | ssdifeq0 3352 | A class is a subclass of itself subtracted from another iff it is the empty set. (Contributed by Steve Rodriguez, 20-Nov-2015.) |
Theorem | ssundifim 3353 | A consequence of inclusion in the union of two classes. In classical logic this would be a biconditional. (Contributed by Jim Kingdon, 4-Aug-2018.) |
Theorem | difdifdirss 3354 | Distributive law for class difference. In classical logic, as in Exercise 4.8 of [Stoll] p. 16, this would be equality rather than subset. (Contributed by Jim Kingdon, 4-Aug-2018.) |
Theorem | uneqdifeqim 3355 | Two ways that and can "partition" (when and don't overlap and is a part of ). In classical logic, the second implication would be a biconditional. (Contributed by Jim Kingdon, 4-Aug-2018.) |
Theorem | r19.2m 3356* | Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1572). The restricted version is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) |
Theorem | r19.3rm 3357* | Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 19-Dec-2018.) |
Theorem | r19.28m 3358* | Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) |
Theorem | r19.3rmv 3359* | Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 6-Aug-2018.) |
Theorem | r19.9rmv 3360* | Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 5-Aug-2018.) |
Theorem | r19.28mv 3361* | Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 6-Aug-2018.) |
Theorem | r19.45mv 3362* | Restricted version of Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.) |
Theorem | r19.44mv 3363* | Restricted version of Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.) |
Theorem | r19.27m 3364* | Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) |
Theorem | r19.27mv 3365* | Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) |
Theorem | rzal 3366* | Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | rexn0 3367* | Restricted existential quantification implies its restriction is nonempty (it is also inhabited as shown in rexm 3368). (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) |
Theorem | rexm 3368* | Restricted existential quantification implies its restriction is inhabited. (Contributed by Jim Kingdon, 16-Oct-2018.) |
Theorem | ralidm 3369* | Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997.) |
Theorem | ral0 3370 | Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.) |
Theorem | rgenm 3371* | Generalization rule that eliminates an inhabited class requirement. (Contributed by Jim Kingdon, 5-Aug-2018.) |
Theorem | ralf0 3372* | The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005.) |
Theorem | ralm 3373 | Inhabited classes and restricted quantification. (Contributed by Jim Kingdon, 6-Aug-2018.) |
Theorem | raaanlem 3374* | Special case of raaan 3375 where is inhabited. (Contributed by Jim Kingdon, 6-Aug-2018.) |
Theorem | raaan 3375* | Rearrange restricted quantifiers. (Contributed by NM, 26-Oct-2010.) |
Theorem | raaanv 3376* | Rearrange restricted quantifiers. (Contributed by NM, 11-Mar-1997.) |
Theorem | sbss 3377* | Set substitution into the first argument of a subset relation. (Contributed by Rodolfo Medina, 7-Jul-2010.) (Proof shortened by Mario Carneiro, 14-Nov-2016.) |
Theorem | sbcssg 3378 | Distribute proper substitution through a subclass relation. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Alexander van der Vekens, 23-Jul-2017.) |
Syntax | cif 3379 | Extend class notation to include the conditional operator. See df-if 3380 for a description. (In older databases this was denoted "ded".) |
Definition | df-if 3380* |
Define the conditional operator. Read as "if
then
else ." See iftrue 3384 and iffalse 3387 for its
values. In mathematical literature, this operator is rarely defined
formally but is implicit in informal definitions such as "let
f(x)=0 if
x=0 and 1/x otherwise."
In the absence of excluded middle, this will tend to be useful where is decidable (in the sense of df-dc 779). (Contributed by NM, 15-May-1999.) |
Theorem | dfif6 3381* | An alternate definition of the conditional operator df-if 3380 as a simple class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.) |
Theorem | ifeq1 3382 | Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | ifeq2 3383 | Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | iftrue 3384 | Value of the conditional operator when its first argument is true. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | iftruei 3385 | Inference associated with iftrue 3384. (Contributed by BJ, 7-Oct-2018.) |
Theorem | iftrued 3386 | Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | iffalse 3387 | Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.) |
Theorem | iffalsei 3388 | Inference associated with iffalse 3387. (Contributed by BJ, 7-Oct-2018.) |
Theorem | iffalsed 3389 | Value of the conditional operator when its first argument is false. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | ifnefalse 3390 | When values are unequal, but an "if" condition checks if they are equal, then the "false" branch results. This is a simple utility to provide a slight shortening and simplification of proofs vs. applying iffalse 3387 directly in this case. (Contributed by David A. Wheeler, 15-May-2015.) |
Theorem | ifsbdc 3391 | Distribute a function over an if-clause. (Contributed by Jim Kingdon, 1-Jan-2022.) |
DECID | ||
Theorem | dfif3 3392* | Alternate definition of the conditional operator df-if 3380. Note that is independent of i.e. a constant true or false. (Contributed by NM, 25-Aug-2013.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | ifeq12 3393 | Equality theorem for conditional operators. (Contributed by NM, 1-Sep-2004.) |
Theorem | ifeq1d 3394 | Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
Theorem | ifeq2d 3395 | Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
Theorem | ifeq12d 3396 | Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.) |
Theorem | ifbi 3397 | Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.) |
Theorem | ifbid 3398 | Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.) |
Theorem | ifbieq1d 3399 | Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018.) |
Theorem | ifbieq2i 3400 | Equivalence/equality inference for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |