Home | Intuitionistic Logic Explorer Theorem List (p. 35 of 132) | < 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 | difid 3401 | 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 3402 | 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 3401. (Contributed by David Abernethy, 17-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | dif0 3403 | 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 3404 | 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 3405 | A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.) |
Theorem | difin0 3406 | 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 3407 | 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 3408 | 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 3409 | Absorption of difference by union. (Contributed by NM, 18-Aug-2013.) |
Theorem | inundifss 3410 | 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 | disjdif2 3411 | The difference of a class and a class disjoint from it is the original class. (Contributed by BJ, 21-Apr-2019.) |
Theorem | difun2 3412 | Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
Theorem | undifss 3413 | Union of complementary parts into whole. (Contributed by Jim Kingdon, 4-Aug-2018.) |
Theorem | ssdifin0 3414 | 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 3415 | 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 3416 | 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 3417 | 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 3418 | 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 3419* | Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1602). The restricted version is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) (Revised by Jim Kingdon, 7-Apr-2023.) |
Theorem | r19.2mOLD 3420* | Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1602). The restricted version is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) Obsolete version of r19.2m 3419 as of 7-Apr-2023. (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | r19.3rm 3421* | Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 19-Dec-2018.) |
Theorem | r19.28m 3422* | 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 3423* | Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 6-Aug-2018.) |
Theorem | r19.9rmv 3424* | Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 5-Aug-2018.) |
Theorem | r19.28mv 3425* | 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 3426* | Restricted version of Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.) |
Theorem | r19.44mv 3427* | Restricted version of Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.) |
Theorem | r19.27m 3428* | 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 3429* | 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 3430* | Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | rexn0 3431* | Restricted existential quantification implies its restriction is nonempty (it is also inhabited as shown in rexm 3432). (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) |
Theorem | rexm 3432* | Restricted existential quantification implies its restriction is inhabited. (Contributed by Jim Kingdon, 16-Oct-2018.) |
Theorem | ralidm 3433* | Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997.) |
Theorem | ral0 3434 | Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.) |
Theorem | rgenm 3435* | Generalization rule that eliminates an inhabited class requirement. (Contributed by Jim Kingdon, 5-Aug-2018.) |
Theorem | ralf0 3436* | The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005.) |
Theorem | ralm 3437 | Inhabited classes and restricted quantification. (Contributed by Jim Kingdon, 6-Aug-2018.) |
Theorem | raaanlem 3438* | Special case of raaan 3439 where is inhabited. (Contributed by Jim Kingdon, 6-Aug-2018.) |
Theorem | raaan 3439* | Rearrange restricted quantifiers. (Contributed by NM, 26-Oct-2010.) |
Theorem | raaanv 3440* | Rearrange restricted quantifiers. (Contributed by NM, 11-Mar-1997.) |
Theorem | sbss 3441* | 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 3442 | Distribute proper substitution through a subclass relation. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Alexander van der Vekens, 23-Jul-2017.) |
Theorem | dcun 3443 | The union of two decidable classes is decidable. (Contributed by Jim Kingdon, 5-Oct-2022.) |
DECID DECID DECID | ||
Syntax | cif 3444 | Extend class notation to include the conditional operator. See df-if 3445 for a description. (In older databases this was denoted "ded".) |
Definition | df-if 3445* |
Define the conditional operator. Read as "if
then
else ." See iftrue 3449 and iffalse 3452 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 805). (Contributed by NM, 15-May-1999.) |
Theorem | dfif6 3446* | An alternate definition of the conditional operator df-if 3445 as a simple class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.) |
Theorem | ifeq1 3447 | Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | ifeq2 3448 | Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | iftrue 3449 | 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 3450 | Inference associated with iftrue 3449. (Contributed by BJ, 7-Oct-2018.) |
Theorem | iftrued 3451 | Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | iffalse 3452 | Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.) |
Theorem | iffalsei 3453 | Inference associated with iffalse 3452. (Contributed by BJ, 7-Oct-2018.) |
Theorem | iffalsed 3454 | Value of the conditional operator when its first argument is false. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | ifnefalse 3455 | 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 versus applying iffalse 3452 directly in this case. (Contributed by David A. Wheeler, 15-May-2015.) |
Theorem | ifsbdc 3456 | Distribute a function over an if-clause. (Contributed by Jim Kingdon, 1-Jan-2022.) |
DECID | ||
Theorem | dfif3 3457* | Alternate definition of the conditional operator df-if 3445. 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 3458 | Equality theorem for conditional operators. (Contributed by NM, 1-Sep-2004.) |
Theorem | ifeq1d 3459 | Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
Theorem | ifeq2d 3460 | Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
Theorem | ifeq12d 3461 | Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.) |
Theorem | ifbi 3462 | Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.) |
Theorem | ifbid 3463 | Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.) |
Theorem | ifbieq1d 3464 | Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018.) |
Theorem | ifbieq2i 3465 | Equivalence/equality inference for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | ifbieq2d 3466 | Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | ifbieq12i 3467 | Equivalence deduction for conditional operators. (Contributed by NM, 18-Mar-2013.) |
Theorem | ifbieq12d 3468 | Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | nfifd 3469 | Deduction version of nfif 3470. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 13-Oct-2016.) |
Theorem | nfif 3470 | Bound-variable hypothesis builder for a conditional operator. (Contributed by NM, 16-Feb-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | ifcldadc 3471 | Conditional closure. (Contributed by Jim Kingdon, 11-Jan-2022.) |
DECID | ||
Theorem | ifeq1dadc 3472 | Conditional equality. (Contributed by Jim Kingdon, 1-Jan-2022.) |
DECID | ||
Theorem | ifbothdadc 3473 | A formula containing a decidable conditional operator is true when both of its cases are true. (Contributed by Jim Kingdon, 3-Jun-2022.) |
DECID | ||
Theorem | ifbothdc 3474 | A wff containing a conditional operator is true when both of its cases are true. (Contributed by Jim Kingdon, 8-Aug-2021.) |
DECID | ||
Theorem | ifiddc 3475 | Identical true and false arguments in the conditional operator. (Contributed by NM, 18-Apr-2005.) |
DECID | ||
Theorem | eqifdc 3476 | Expansion of an equality with a conditional operator. (Contributed by Jim Kingdon, 28-Jul-2022.) |
DECID | ||
Theorem | ifcldcd 3477 | Membership (closure) of a conditional operator, deduction form. (Contributed by Jim Kingdon, 8-Aug-2021.) |
DECID | ||
Theorem | ifandc 3478 | Rewrite a conjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.) |
DECID | ||
Theorem | ifmdc 3479 | If a conditional class is inhabited, then the condition is decidable. This shows that conditionals are not very useful unless one can prove the condition decidable. (Contributed by BJ, 24-Sep-2022.) |
DECID | ||
Syntax | cpw 3480 | 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 3481* | Soundness justification theorem for df-pw 3482. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Definition | df-pw 3482* | 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 3483 | Equality theorem for power class. (Contributed by NM, 5-Aug-1993.) |
Theorem | pweqi 3484 | Equality inference for power class. (Contributed by NM, 27-Nov-2013.) |
Theorem | pweqd 3485 | Equality deduction for power class. (Contributed by NM, 27-Nov-2013.) |
Theorem | elpw 3486 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.) |
Theorem | velpw 3487* | Setvar variable membership in a power class (common case). See elpw 3486. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | elpwg 3488 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 6-Aug-2000.) |
Theorem | elpwi 3489 | Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.) |
Theorem | elpwb 3490 | Characterization of the elements of a power class. (Contributed by BJ, 29-Apr-2021.) |
Theorem | elpwid 3491 | An element of a power class is a subclass. Deduction form of elpwi 3489. (Contributed by David Moews, 1-May-2017.) |
Theorem | elelpwi 3492 | If belongs to a part of then belongs to . (Contributed by FL, 3-Aug-2009.) |
Theorem | nfpw 3493 | Bound-variable hypothesis builder for power class. (Contributed by NM, 28-Oct-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) |
Theorem | pwidg 3494 | Membership of the original in a power set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
Theorem | pwid 3495 | A set is a member of its power class. Theorem 87 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.) |
Theorem | pwss 3496* | Subclass relationship for power class. (Contributed by NM, 21-Jun-2009.) |
Syntax | csn 3497 | Extend class notation to include singleton. |
Syntax | cpr 3498 | Extend class notation to include unordered pair. |
Syntax | ctp 3499 | Extend class notation to include unordered triplet. |
Syntax | cop 3500 | Extend class notation to include ordered pair. |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |