Home | Intuitionistic Logic Explorer Theorem List (p. 34 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 | disjne 3301 | Members of disjoint sets are not equal. (Contributed by NM, 28-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | disjel 3302 | A set can't belong to both members of disjoint classes. (Contributed by NM, 28-Feb-2015.) |
Theorem | disj2 3303 | Two ways of saying that two classes are disjoint. (Contributed by NM, 17-May-1998.) |
Theorem | disj4im 3304 | A consequence of two classes being disjoint. In classical logic this would be a biconditional. (Contributed by Jim Kingdon, 2-Aug-2018.) |
Theorem | ssdisj 3305 | Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007.) |
Theorem | disjpss 3306 | A class is a proper subset of its union with a disjoint nonempty class. (Contributed by NM, 15-Sep-2004.) |
Theorem | undisj1 3307 | The union of disjoint classes is disjoint. (Contributed by NM, 26-Sep-2004.) |
Theorem | undisj2 3308 | The union of disjoint classes is disjoint. (Contributed by NM, 13-Sep-2004.) |
Theorem | ssindif0im 3309 | Subclass implies empty intersection with difference from the universal class. (Contributed by NM, 17-Sep-2003.) |
Theorem | inelcm 3310 | The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.) |
Theorem | minel 3311 | A minimum element of a class has no elements in common with the class. (Contributed by NM, 22-Jun-1994.) |
Theorem | undif4 3312 | Distribute union over difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | disjssun 3313 | Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | ssdif0im 3314 | 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 3315 | Universal class equality in terms of empty difference. (Contributed by Jim Kingdon, 3-Aug-2018.) |
Theorem | difrab0eqim 3316* | 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 | ssnelpss 3317 | A subclass missing a member is a proper subclass. (Contributed by NM, 12-Jan-2002.) |
Theorem | ssnelpssd 3318 | Subclass inclusion with one element of the superclass missing is proper subclass inclusion. Deduction form of ssnelpss 3317. (Contributed by David Moews, 1-May-2017.) |
Theorem | inssdif0im 3319 | Intersection, subclass, and difference relationship. In classical logic the converse would also hold. (Contributed by Jim Kingdon, 3-Aug-2018.) |
Theorem | difid 3320 | 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 3321 | 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 3320. (Contributed by David Abernethy, 17-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | dif0 3322 | 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 3323 | 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 3324 | A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.) |
Theorem | difin0 3325 | 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 3326 | 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 3327 | 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 3328 | Absorption of difference by union. (Contributed by NM, 18-Aug-2013.) |
Theorem | inundifss 3329 | 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 3330 | Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
Theorem | undifss 3331 | Union of complementary parts into whole. (Contributed by Jim Kingdon, 4-Aug-2018.) |
Theorem | ssdifin0 3332 | 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 3333 | 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 3334 | 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 3335 | 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 3336 | 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 3337* | Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1545). The restricted version is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) |
Theorem | r19.3rm 3338* | Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 19-Dec-2018.) |
Theorem | r19.28m 3339* | 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 3340* | Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 6-Aug-2018.) |
Theorem | r19.9rmv 3341* | Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 5-Aug-2018.) |
Theorem | r19.28mv 3342* | 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 3343* | Restricted version of Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.) |
Theorem | r19.27m 3344* | 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 3345* | 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 3346* | Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | rexn0 3347* | Restricted existential quantification implies its restriction is nonempty (it is also inhabited as shown in rexm 3348). (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) |
Theorem | rexm 3348* | Restricted existential quantification implies its restriction is inhabited. (Contributed by Jim Kingdon, 16-Oct-2018.) |
Theorem | ralidm 3349* | Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997.) |
Theorem | ral0 3350 | Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.) |
Theorem | rgenm 3351* | Generalization rule that eliminates an inhabited class requirement. (Contributed by Jim Kingdon, 5-Aug-2018.) |
Theorem | ralf0 3352* | The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005.) |
Theorem | ralm 3353 | Inhabited classes and restricted quantification. (Contributed by Jim Kingdon, 6-Aug-2018.) |
Theorem | raaanlem 3354* | Special case of raaan 3355 where is inhabited. (Contributed by Jim Kingdon, 6-Aug-2018.) |
Theorem | raaan 3355* | Rearrange restricted quantifiers. (Contributed by NM, 26-Oct-2010.) |
Theorem | raaanv 3356* | Rearrange restricted quantifiers. (Contributed by NM, 11-Mar-1997.) |
Theorem | sbss 3357* | 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 3358 | 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 3359 | Extend class notation to include the conditional operator. See df-if 3360 for a description. (In older databases this was denoted "ded".) |
Definition | df-if 3360* |
Define the conditional operator. Read as "if
then
else ." See iftrue 3364 and iffalse 3367 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 754). (Contributed by NM, 15-May-1999.) |
Theorem | dfif6 3361* | An alternate definition of the conditional operator df-if 3360 as a simple class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.) |
Theorem | ifeq1 3362 | Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | ifeq2 3363 | Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | iftrue 3364 | 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 3365 | Inference associated with iftrue 3364. (Contributed by BJ, 7-Oct-2018.) |
Theorem | iftrued 3366 | Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | iffalse 3367 | Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.) |
Theorem | iffalsei 3368 | Inference associated with iffalse 3367. (Contributed by BJ, 7-Oct-2018.) |
Theorem | iffalsed 3369 | Value of the conditional operator when its first argument is false. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | ifnefalse 3370 | 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 3367 directly in this case. (Contributed by David A. Wheeler, 15-May-2015.) |
Theorem | dfif3 3371* | Alternate definition of the conditional operator df-if 3360. 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 3372 | Equality theorem for conditional operators. (Contributed by NM, 1-Sep-2004.) |
Theorem | ifeq1d 3373 | Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
Theorem | ifeq2d 3374 | Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
Theorem | ifeq12d 3375 | Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.) |
Theorem | ifbi 3376 | Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.) |
Theorem | ifbid 3377 | Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.) |
Theorem | ifbieq1d 3378 | Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018.) |
Theorem | ifbieq2i 3379 | Equivalence/equality inference for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | ifbieq2d 3380 | Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | ifbieq12i 3381 | Equivalence deduction for conditional operators. (Contributed by NM, 18-Mar-2013.) |
Theorem | ifbieq12d 3382 | Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | nfifd 3383 | Deduction version of nfif 3384. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 13-Oct-2016.) |
Theorem | nfif 3384 | Bound-variable hypothesis builder for a conditional operator. (Contributed by NM, 16-Feb-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | ifbothdc 3385 | A wff containing a conditional operator is true when both of its cases are true. (Contributed by Jim Kingdon, 8-Aug-2021.) |
DECID | ||
Theorem | ifcldcd 3386 | Membership (closure) of a conditional operator, deduction form. (Contributed by Jim Kingdon, 8-Aug-2021.) |
DECID | ||
Syntax | cpw 3387 | Extend class notation to include power class. (The tilde in the Metamath token is meant to suggest the calligraphic font of the P.) |
Theorem | pwjust 3388* | Soundness justification theorem for df-pw 3389. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Definition | df-pw 3389* | Define power class. Definition 5.10 of [TakeutiZaring] p. 17, but we also let it apply to proper classes, i.e. those that are not members of . When applied to a set, this produces its power set. A power set of S is the set of all subsets of S, including the empty set and S itself. For example, if is { 3 , 5 , 7 }, then is { (/) , { 3 } , { 5 } , { 7 } , { 3 , 5 } , { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } }. We will later introduce the Axiom of Power Sets. Still later we will prove that the size of the power set of a finite set is 2 raised to the power of the size of the set. (Contributed by NM, 5-Aug-1993.) |
Theorem | pweq 3390 | Equality theorem for power class. (Contributed by NM, 5-Aug-1993.) |
Theorem | pweqi 3391 | Equality inference for power class. (Contributed by NM, 27-Nov-2013.) |
Theorem | pweqd 3392 | Equality deduction for power class. (Contributed by NM, 27-Nov-2013.) |
Theorem | elpw 3393 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.) |
Theorem | selpw 3394* | Setvar variable membership in a power class (common case). See elpw 3393. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | elpwg 3395 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 6-Aug-2000.) |
Theorem | elpwi 3396 | Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.) |
Theorem | elpwid 3397 | An element of a power class is a subclass. Deduction form of elpwi 3396. (Contributed by David Moews, 1-May-2017.) |
Theorem | elelpwi 3398 | If belongs to a part of then belongs to . (Contributed by FL, 3-Aug-2009.) |
Theorem | nfpw 3399 | Bound-variable hypothesis builder for power class. (Contributed by NM, 28-Oct-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) |
Theorem | pwidg 3400 | Membership of the original in a power set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |