![]() |
Intuitionistic Logic Explorer Theorem List (p. 36 of 152) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | difrab0eqim 3501* | 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 3502 | Intersection, subclass, and difference relationship. In classical logic the converse would also hold. (Contributed by Jim Kingdon, 3-Aug-2018.) |
⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐶 → (𝐴 ∩ (𝐵 ∖ 𝐶)) = ∅) | ||
Theorem | difid 3503 | 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 3504 | 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 3503. (Contributed by David Abernethy, 17-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∖ 𝐴) = ∅ | ||
Theorem | dif0 3505 | 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 3506 | 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 3507 | A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.) |
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ | ||
Theorem | difin0 3508 | 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 3509 | 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 3510 | 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 3511 | Absorption of difference by union. (Contributed by NM, 18-Aug-2013.) |
⊢ (𝐴 ∪ (𝐴 ∖ 𝐵)) = 𝐴 | ||
Theorem | inundifss 3512 | 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 3513 | The difference of a class and a class disjoint from it is the original class. (Contributed by BJ, 21-Apr-2019.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∖ 𝐵) = 𝐴) | ||
Theorem | difun2 3514 | Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) | ||
Theorem | undifss 3515 | Union of complementary parts into whole. (Contributed by Jim Kingdon, 4-Aug-2018.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) ⊆ 𝐵) | ||
Theorem | ssdifin0 3516 | 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 3517 | 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 3518 | 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 3519 | 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 3520 | 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 3521* | Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1648). 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 3522* | Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1648). 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 3521 as of 7-Apr-2023. (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | r19.3rm 3523* | Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 19-Dec-2018.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | r19.28m 3524* | 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 3525* | Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 6-Aug-2018.) |
⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | r19.9rmv 3526* | Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 5-Aug-2018.) |
⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | r19.28mv 3527* | 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 3528* | Restricted version of Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.) |
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))) | ||
Theorem | r19.44mv 3529* | Restricted version of Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.) |
⊢ (∃𝑦 𝑦 ∈ 𝐴 → (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ 𝜓))) | ||
Theorem | r19.27m 3530* | 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 3531* | 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 3532* | Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexn0 3533* | Restricted existential quantification implies its restriction is nonempty (it is also inhabited as shown in rexm 3534). (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅) | ||
Theorem | rexm 3534* | Restricted existential quantification implies its restriction is inhabited. (Contributed by Jim Kingdon, 16-Oct-2018.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | ralidm 3535* | Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ral0 3536 | Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.) |
⊢ ∀𝑥 ∈ ∅ 𝜑 | ||
Theorem | rgenm 3537* | Generalization rule that eliminates an inhabited class requirement. (Contributed by Jim Kingdon, 5-Aug-2018.) |
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝜑) ⇒ ⊢ ∀𝑥 ∈ 𝐴 𝜑 | ||
Theorem | ralf0 3538* | The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005.) |
⊢ ¬ 𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 = ∅) | ||
Theorem | ralm 3539 | Inhabited classes and restricted quantification. (Contributed by Jim Kingdon, 6-Aug-2018.) |
⊢ ((∃𝑥 𝑥 ∈ 𝐴 → ∀𝑥 ∈ 𝐴 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | raaanlem 3540* | Special case of raaan 3541 where 𝐴 is inhabited. (Contributed by Jim Kingdon, 6-Aug-2018.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓))) | ||
Theorem | raaan 3541* | Rearrange restricted quantifiers. (Contributed by NM, 26-Oct-2010.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓)) | ||
Theorem | raaanv 3542* | Rearrange restricted quantifiers. (Contributed by NM, 11-Mar-1997.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓)) | ||
Theorem | sbss 3543* | 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 3544 | 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 3545 | The union of two decidable classes is decidable. (Contributed by Jim Kingdon, 5-Oct-2022.) |
⊢ (𝜑 → DECID 𝑘 ∈ 𝐴) & ⊢ (𝜑 → DECID 𝑘 ∈ 𝐵) ⇒ ⊢ (𝜑 → DECID 𝑘 ∈ (𝐴 ∪ 𝐵)) | ||
Syntax | cif 3546 | Extend class notation to include the conditional operator. See df-if 3547 for a description. (In older databases this was denoted "ded".) |
class if(𝜑, 𝐴, 𝐵) | ||
Definition | df-if 3547* |
Define the conditional operator. Read if(𝜑, 𝐴, 𝐵) as "if
𝜑 then 𝐴 else 𝐵".
See iftrue 3551 and iffalse 3554 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 836). (Contributed by NM, 15-May-1999.) |
⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} | ||
Theorem | dfif6 3548* | An alternate definition of the conditional operator df-if 3547 as a simple class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.) |
⊢ if(𝜑, 𝐴, 𝐵) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ ¬ 𝜑}) | ||
Theorem | ifeq1 3549 | Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 = 𝐵 → if(𝜑, 𝐴, 𝐶) = if(𝜑, 𝐵, 𝐶)) | ||
Theorem | ifeq2 3550 | Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 = 𝐵 → if(𝜑, 𝐶, 𝐴) = if(𝜑, 𝐶, 𝐵)) | ||
Theorem | iftrue 3551 | 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.) |
⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | ||
Theorem | iftruei 3552 | Inference associated with iftrue 3551. (Contributed by BJ, 7-Oct-2018.) |
⊢ 𝜑 ⇒ ⊢ if(𝜑, 𝐴, 𝐵) = 𝐴 | ||
Theorem | iftrued 3553 | Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴) | ||
Theorem | iffalse 3554 | Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.) |
⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | ||
Theorem | iffalsei 3555 | Inference associated with iffalse 3554. (Contributed by BJ, 7-Oct-2018.) |
⊢ ¬ 𝜑 ⇒ ⊢ if(𝜑, 𝐴, 𝐵) = 𝐵 | ||
Theorem | iffalsed 3556 | Value of the conditional operator when its first argument is false. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐵) | ||
Theorem | ifnefalse 3557 | 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 3554 directly in this case. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷) | ||
Theorem | ifsbdc 3558 | Distribute a function over an if-clause. (Contributed by Jim Kingdon, 1-Jan-2022.) |
⊢ (if(𝜑, 𝐴, 𝐵) = 𝐴 → 𝐶 = 𝐷) & ⊢ (if(𝜑, 𝐴, 𝐵) = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ (DECID 𝜑 → 𝐶 = if(𝜑, 𝐷, 𝐸)) | ||
Theorem | dfif3 3559* | Alternate definition of the conditional operator df-if 3547. 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.) |
⊢ 𝐶 = {𝑥 ∣ 𝜑} ⇒ ⊢ if(𝜑, 𝐴, 𝐵) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ (V ∖ 𝐶))) | ||
Theorem | ifssun 3560 | A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.) |
⊢ if(𝜑, 𝐴, 𝐵) ⊆ (𝐴 ∪ 𝐵) | ||
Theorem | ifidss 3561 | A conditional class whose two alternatives are equal is included in that alternative. With excluded middle, we can prove it is equal to it. (Contributed by BJ, 15-Aug-2024.) |
⊢ if(𝜑, 𝐴, 𝐴) ⊆ 𝐴 | ||
Theorem | ifeq12 3562 | Equality theorem for conditional operators. (Contributed by NM, 1-Sep-2004.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → if(𝜑, 𝐴, 𝐶) = if(𝜑, 𝐵, 𝐷)) | ||
Theorem | ifeq1d 3563 | Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) | ||
Theorem | ifeq2d 3564 | Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) | ||
Theorem | ifeq12d 3565 | Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷)) | ||
Theorem | ifbi 3566 | Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.) |
⊢ ((𝜑 ↔ 𝜓) → if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵)) | ||
Theorem | ifbid 3567 | Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵)) | ||
Theorem | ifbieq1d 3568 | Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶)) | ||
Theorem | ifbieq2i 3569 | Equivalence/equality inference for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ 𝐴 = 𝐵 ⇒ ⊢ if(𝜑, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵) | ||
Theorem | ifbieq2d 3570 | Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵)) | ||
Theorem | ifbieq12i 3571 | Equivalence deduction for conditional operators. (Contributed by NM, 18-Mar-2013.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐶, 𝐷) | ||
Theorem | ifbieq12d 3572 | Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷)) | ||
Theorem | nfifd 3573 | Deduction version of nfif 3574. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥if(𝜓, 𝐴, 𝐵)) | ||
Theorem | nfif 3574 | Bound-variable hypothesis builder for a conditional operator. (Contributed by NM, 16-Feb-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥if(𝜑, 𝐴, 𝐵) | ||
Theorem | ifcldadc 3575 | Conditional closure. (Contributed by Jim Kingdon, 11-Jan-2022.) |
⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶) & ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶) & ⊢ (𝜑 → DECID 𝜓) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶) | ||
Theorem | ifeq1dadc 3576 | Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐵) & ⊢ (𝜑 → DECID 𝜓) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) | ||
Theorem | ifeq2dadc 3577 | Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐴 = 𝐵) & ⊢ (𝜑 → DECID 𝜓) ⇒ ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) | ||
Theorem | ifbothdadc 3578 | A formula 𝜃 containing a decidable conditional operator is true when both of its cases are true. (Contributed by Jim Kingdon, 3-Jun-2022.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) & ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) & ⊢ ((𝜂 ∧ 𝜑) → 𝜓) & ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒) & ⊢ (𝜂 → DECID 𝜑) ⇒ ⊢ (𝜂 → 𝜃) | ||
Theorem | ifbothdc 3579 | A wff 𝜃 containing a conditional operator is true when both of its cases are true. (Contributed by Jim Kingdon, 8-Aug-2021.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) & ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ DECID 𝜑) → 𝜃) | ||
Theorem | ifiddc 3580 | Identical true and false arguments in the conditional operator. (Contributed by NM, 18-Apr-2005.) |
⊢ (DECID 𝜑 → if(𝜑, 𝐴, 𝐴) = 𝐴) | ||
Theorem | eqifdc 3581 | Expansion of an equality with a conditional operator. (Contributed by Jim Kingdon, 28-Jul-2022.) |
⊢ (DECID 𝜑 → (𝐴 = if(𝜑, 𝐵, 𝐶) ↔ ((𝜑 ∧ 𝐴 = 𝐵) ∨ (¬ 𝜑 ∧ 𝐴 = 𝐶)))) | ||
Theorem | ifcldcd 3582 | Membership (closure) of a conditional operator, deduction form. (Contributed by Jim Kingdon, 8-Aug-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐶) & ⊢ (𝜑 → DECID 𝜓) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶) | ||
Theorem | ifnotdc 3583 | Negating the first argument swaps the last two arguments of a conditional operator. (Contributed by NM, 21-Jun-2007.) |
⊢ (DECID 𝜑 → if(¬ 𝜑, 𝐴, 𝐵) = if(𝜑, 𝐵, 𝐴)) | ||
Theorem | ifandc 3584 | Rewrite a conjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (DECID 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)) | ||
Theorem | ifordc 3585 | Rewrite a disjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (DECID 𝜑 → if((𝜑 ∨ 𝜓), 𝐴, 𝐵) = if(𝜑, 𝐴, if(𝜓, 𝐴, 𝐵))) | ||
Theorem | ifmdc 3586 | 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.) |
⊢ (𝐴 ∈ if(𝜑, 𝐵, 𝐶) → DECID 𝜑) | ||
Syntax | cpw 3587 | Extend class notation to include power class. (The tilde in the Metamath token is meant to suggest the calligraphic font of the P.) |
class 𝒫 𝐴 | ||
Theorem | pwjust 3588* | Soundness justification theorem for df-pw 3589. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ {𝑥 ∣ 𝑥 ⊆ 𝐴} = {𝑦 ∣ 𝑦 ⊆ 𝐴} | ||
Definition | df-pw 3589* | 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 V. 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 3590 | Equality theorem for power class. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) | ||
Theorem | pweqi 3591 | Equality inference for power class. (Contributed by NM, 27-Nov-2013.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ 𝒫 𝐴 = 𝒫 𝐵 | ||
Theorem | pweqd 3592 | Equality deduction for power class. (Contributed by NM, 27-Nov-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵) | ||
Theorem | elpw 3593 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) | ||
Theorem | velpw 3594* | Setvar variable membership in a power class (common case). See elpw 3593. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) | ||
Theorem | elpwg 3595 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 6-Aug-2000.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | elpwi 3596 | Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.) |
⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵) | ||
Theorem | elpwb 3597 | Characterization of the elements of a power class. (Contributed by BJ, 29-Apr-2021.) |
⊢ (𝐴 ∈ 𝒫 𝐵 ↔ (𝐴 ∈ V ∧ 𝐴 ⊆ 𝐵)) | ||
Theorem | elpwid 3598 | An element of a power class is a subclass. Deduction form of elpwi 3596. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | elelpwi 3599 | If 𝐴 belongs to a part of 𝐶 then 𝐴 belongs to 𝐶. (Contributed by FL, 3-Aug-2009.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝒫 𝐶) → 𝐴 ∈ 𝐶) | ||
Theorem | nfpw 3600 | Bound-variable hypothesis builder for power class. (Contributed by NM, 28-Oct-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥𝒫 𝐴 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |