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