Home | Metamath
Proof Explorer Theorem List (p. 41 of 426) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | csbnest1g 4001 | Nest the composition of two substitutions. (Contributed by NM, 23-May-2006.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑥⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑥⦌𝐶) | ||
Theorem | csbidm 4002* | Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008.) (Revised by NM, 18-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | csbvarg 4003 | The proper substitution of a class for setvar variable results in the class (if the class exists). (Contributed by NM, 10-Nov-2005.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) | ||
Theorem | sbccsb 4004* | Substitution into a wff expressed in terms of substitution into a class. (Contributed by NM, 15-Aug-2007.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑}) | ||
Theorem | sbccsb2 4005 | Substitution into a wff expressed in using substitution into a class. (Contributed by NM, 27-Nov-2005.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ ⦋𝐴 / 𝑥⦌{𝑥 ∣ 𝜑}) | ||
Theorem | rspcsbela 4006* | Special case related to rspsbc 3518. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷) | ||
Theorem | sbnfc2 4007* | Two ways of expressing "𝑥 is (effectively) not free in 𝐴." (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴) | ||
Theorem | csbab 4008* | Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005.) (Revised by NM, 19-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑} = {𝑦 ∣ [𝐴 / 𝑥]𝜑} | ||
Theorem | csbun 4009 | Distribution of class substitution over union of two classes. (Contributed by Drahflow, 23-Sep-2015.) (Revised by Mario Carneiro, 11-Dec-2016.) (Revised by NM, 13-Sep-2018.) |
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∪ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∪ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | csbin 4010 | Distribute proper substitution into a class through an intersection relation. (Contributed by Alan Sare, 22-Jul-2012.) (Revised by NM, 18-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | un00 4011 | Two classes are empty iff their union is empty. (Contributed by NM, 11-Aug-2004.) |
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 ∪ 𝐵) = ∅) | ||
Theorem | vss 4012 | 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.) |
⊢ (V ⊆ 𝐴 ↔ 𝐴 = V) | ||
Theorem | 0pss 4013 | The null set is a proper subset of any nonempty set. (Contributed by NM, 27-Feb-1996.) |
⊢ (∅ ⊊ 𝐴 ↔ 𝐴 ≠ ∅) | ||
Theorem | npss0 4014 | No set is a proper subset of the empty set. (Contributed by NM, 17-Jun-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ ¬ 𝐴 ⊊ ∅ | ||
Theorem | npss0OLD 4015 | Obsolete proof of npss0 4014 as of 14-Jul-2021. (Contributed by NM, 17-Jun-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ¬ 𝐴 ⊊ ∅ | ||
Theorem | pssv 4016 | Any non-universal class is a proper subclass of the universal class. (Contributed by NM, 17-May-1998.) |
⊢ (𝐴 ⊊ V ↔ ¬ 𝐴 = V) | ||
Theorem | disj 4017* | Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) | ||
Theorem | disjr 4018* | Two ways of saying that two classes are disjoint. (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ 𝐴) | ||
Theorem | disj1 4019* | Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 19-Aug-1993.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) | ||
Theorem | reldisj 4020 | 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 4021 | Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 = (𝐴 ∖ 𝐵)) | ||
Theorem | disjne 4022 | Members of disjoint sets are not equal. (Contributed by NM, 28-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → 𝐶 ≠ 𝐷) | ||
Theorem | disjel 4023 | A set can't belong to both members of disjoint classes. (Contributed by NM, 28-Feb-2015.) |
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴) → ¬ 𝐶 ∈ 𝐵) | ||
Theorem | disj2 4024 | Two ways of saying that two classes are disjoint. (Contributed by NM, 17-May-1998.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (V ∖ 𝐵)) | ||
Theorem | disj4 4025 | Two ways of saying that two classes are disjoint. (Contributed by NM, 21-Mar-2004.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ¬ (𝐴 ∖ 𝐵) ⊊ 𝐴) | ||
Theorem | ssdisj 4026 | Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (𝐴 ∩ 𝐶) = ∅) | ||
Theorem | ssdisjOLD 4027 | Obsolete proof of ssdisj 4026 as of 14-Jul-2021. (Contributed by FL, 24-Jan-2007.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (𝐴 ∩ 𝐶) = ∅) | ||
Theorem | disjpss 4028 | A class is a proper subset of its union with a disjoint nonempty class. (Contributed by NM, 15-Sep-2004.) |
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐵 ≠ ∅) → 𝐴 ⊊ (𝐴 ∪ 𝐵)) | ||
Theorem | undisj1 4029 | The union of disjoint classes is disjoint. (Contributed by NM, 26-Sep-2004.) |
⊢ (((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐶) = ∅) ↔ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ∅) | ||
Theorem | undisj2 4030 | The union of disjoint classes is disjoint. (Contributed by NM, 13-Sep-2004.) |
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ (𝐴 ∩ 𝐶) = ∅) ↔ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ∅) | ||
Theorem | ssindif0 4031 | Subclass expressed in terms of intersection with difference from the universal class. (Contributed by NM, 17-Sep-2003.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ (V ∖ 𝐵)) = ∅) | ||
Theorem | inelcm 4032 | The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅) | ||
Theorem | minel 4033 | A minimum element of a class has no elements in common with the class. (Contributed by NM, 22-Jun-1994.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ ((𝐴 ∈ 𝐵 ∧ (𝐶 ∩ 𝐵) = ∅) → ¬ 𝐴 ∈ 𝐶) | ||
Theorem | minelOLD 4034 | Obsolete proof of minel 4033 as of 14-Jul-2021. (Contributed by NM, 22-Jun-1994.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ 𝐵 ∧ (𝐶 ∩ 𝐵) = ∅) → ¬ 𝐴 ∈ 𝐶) | ||
Theorem | undif4 4035 | Distribute union over difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐶) = ∅ → (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)) | ||
Theorem | disjssun 4036 | Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ 𝐴 ⊆ 𝐶)) | ||
Theorem | vdif0 4037 | Universal class equality in terms of empty difference. (Contributed by NM, 17-Sep-2003.) |
⊢ (𝐴 = V ↔ (V ∖ 𝐴) = ∅) | ||
Theorem | difrab0eq 4038* | 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 Alexander van der Vekens, 31-Dec-2017.) |
⊢ ((𝑉 ∖ {𝑥 ∈ 𝑉 ∣ 𝜑}) = ∅ ↔ 𝑉 = {𝑥 ∈ 𝑉 ∣ 𝜑}) | ||
Theorem | pssnel 4039* | A proper subclass has a member in one argument that's not in both. (Contributed by NM, 29-Feb-1996.) |
⊢ (𝐴 ⊊ 𝐵 → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) | ||
Theorem | disjdif 4040 | A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.) |
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ | ||
Theorem | difin0 4041 | 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 | unvdif 4042 | The union of a class and its complement is the universe. Theorem 5.1(5) of [Stoll] p. 17. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∪ (V ∖ 𝐴)) = V | ||
Theorem | undif1 4043 | Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4040). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) | ||
Theorem | undif2 4044 | Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4040). Part of proof of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 19-May-1998.) |
⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) | ||
Theorem | undifabs 4045 | Absorption of difference by union. (Contributed by NM, 18-Aug-2013.) |
⊢ (𝐴 ∪ (𝐴 ∖ 𝐵)) = 𝐴 | ||
Theorem | inundif 4046 | The intersection and class difference of a class with another class unite to give the original class. (Contributed by Paul Chapman, 5-Jun-2009.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴 | ||
Theorem | disjdif2 4047 | The difference of a class and a class disjoint from it is the original class. (Contributed by BJ, 21-Apr-2019.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∖ 𝐵) = 𝐴) | ||
Theorem | difun2 4048 | Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) | ||
Theorem | undif 4049 | Union of complementary parts into whole. (Contributed by NM, 22-Mar-1998.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵) | ||
Theorem | ssdifin0 4050 | 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 4051 | A class is a subclass of itself subtracted from another iff it is the empty set. (Contributed by Steve Rodriguez, 20-Nov-2015.) |
⊢ (𝐴 ⊆ (𝐵 ∖ 𝐴) ↔ 𝐴 = ∅) | ||
Theorem | ssundif 4052 | A condition equivalent to inclusion in the union of two classes. (Contributed by NM, 26-Mar-2007.) |
⊢ (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐵) ⊆ 𝐶) | ||
Theorem | difcom 4053 | Swap the arguments of a class difference. (Contributed by NM, 29-Mar-2007.) |
⊢ ((𝐴 ∖ 𝐵) ⊆ 𝐶 ↔ (𝐴 ∖ 𝐶) ⊆ 𝐵) | ||
Theorem | pssdifcom1 4054 | Two ways to express overlapping subsets. (Contributed by Stefan O'Rear, 31-Oct-2014.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → ((𝐶 ∖ 𝐴) ⊊ 𝐵 ↔ (𝐶 ∖ 𝐵) ⊊ 𝐴)) | ||
Theorem | pssdifcom2 4055 | Two ways to express non-covering pairs of subsets. (Contributed by Stefan O'Rear, 31-Oct-2014.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐵 ⊊ (𝐶 ∖ 𝐴) ↔ 𝐴 ⊊ (𝐶 ∖ 𝐵))) | ||
Theorem | difdifdir 4056 | Distributive law for class difference. Exercise 4.8 of [Stoll] p. 16. (Contributed by NM, 18-Aug-2004.) |
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ (𝐵 ∖ 𝐶)) | ||
Theorem | uneqdifeq 4057 | Two ways to say that 𝐴 and 𝐵 partition 𝐶 (when 𝐴 and 𝐵 don't overlap and 𝐴 is a part of 𝐶). (Contributed by FL, 17-Nov-2008.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 ↔ (𝐶 ∖ 𝐴) = 𝐵)) | ||
Theorem | uneqdifeqOLD 4058 | Obsolete proof of uneqdifeq 4057 as of 14-Jul-2021. (Contributed by FL, 17-Nov-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 ↔ (𝐶 ∖ 𝐴) = 𝐵)) | ||
Theorem | raldifeq 4059* | Equality theorem for restricted universal quantifier. (Contributed by Thierry Arnoux, 6-Jul-2019.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → ∀𝑥 ∈ (𝐵 ∖ 𝐴)𝜓) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | r19.2z 4060* | Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1892). The restricted version is valid only when the domain of quantification is not empty. (Contributed by NM, 15-Nov-2003.) |
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | r19.2zb 4061* | A response to the notion that the condition 𝐴 ≠ ∅ can be removed in r19.2z 4060. Interestingly enough, 𝜑 does not figure in the left-hand side. (Contributed by Jeff Hankins, 24-Aug-2009.) |
⊢ (𝐴 ≠ ∅ ↔ (∀𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | r19.3rz 4062* | Restricted quantification of wff not containing quantified variable. (Contributed by FL, 3-Jan-2008.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | r19.28z 4063* | Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by NM, 26-Oct-2010.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))) | ||
Theorem | r19.3rzv 4064* | Restricted quantification of wff not containing quantified variable. (Contributed by NM, 10-Mar-1997.) |
⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | r19.9rzv 4065* | Restricted quantification of wff not containing quantified variable. (Contributed by NM, 27-May-1998.) |
⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | r19.28zv 4066* | Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by NM, 19-Aug-2004.) |
⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))) | ||
Theorem | r19.37zv 4067* | Restricted quantifier version of Theorem 19.37 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by Paul Chapman, 8-Oct-2007.) |
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓))) | ||
Theorem | r19.45zv 4068* | Restricted version of Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.) |
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓))) | ||
Theorem | r19.44zv 4069* | Restricted version of Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.) |
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ 𝜓))) | ||
Theorem | r19.27z 4070* | Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by NM, 26-Oct-2010.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))) | ||
Theorem | r19.27zv 4071* | Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by NM, 19-Aug-2004.) |
⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))) | ||
Theorem | r19.36zv 4072* | Restricted quantifier version of Theorem 19.36 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by NM, 20-Sep-2003.) |
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 → 𝜓))) | ||
Theorem | rzal 4073* | Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexn0 4074* | Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅) | ||
Theorem | ralidm 4075* | Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ral0 4076 | Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.) |
⊢ ∀𝑥 ∈ ∅ 𝜑 | ||
Theorem | rgenzOLD 4077* | Obsolete as of 22-Jul-2021. (Contributed by NM, 8-Dec-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐴 ≠ ∅ ∧ 𝑥 ∈ 𝐴) → 𝜑) ⇒ ⊢ ∀𝑥 ∈ 𝐴 𝜑 | ||
Theorem | ralf0 4078* | The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ ¬ 𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 = ∅) | ||
Theorem | ralf0OLD 4079* | Obsolete proof of ralf0 4078 as of 14-Jul-2021. (Contributed by NM, 26-Nov-2005.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ¬ 𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 = ∅) | ||
Theorem | ralnralall 4080* | A contradiction concerning restricted generalization for a nonempty set implies anything. (Contributed by Alexander van der Vekens, 4-Sep-2018.) |
⊢ (𝐴 ≠ ∅ → ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ¬ 𝜑) → 𝜓)) | ||
Theorem | falseral0 4081* | A false statement can only be true for elements of an empty set. (Contributed by AV, 30-Oct-2020.) |
⊢ ((∀𝑥 ¬ 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜑) → 𝐴 = ∅) | ||
Theorem | raaan 4082* | Rearrange restricted quantifiers. (Contributed by NM, 26-Oct-2010.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓)) | ||
Theorem | raaanv 4083* | Rearrange restricted quantifiers. (Contributed by NM, 11-Mar-1997.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓)) | ||
Theorem | sbss 4084* | 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 4085 | Distribute proper substitution through a subclass relation. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Alexander van der Vekens, 23-Jul-2017.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ⊆ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ⊆ ⦋𝐴 / 𝑥⦌𝐶)) | ||
In a Hilbert system of logic (which consists of a set of axioms, modus ponens, and the generalization rule), converting a deduction to a proof using the Deduction Theorem (taught in introductory logic books) involves an exponential increase of the number of steps as hypotheses are successively eliminated. Here is a trick that is not as general as the Deduction Theorem but requires only a linear increase in the number of steps. The general problem: We want to convert a deduction P |- Q into a proof of the theorem |- P -> Q i.e., we want to eliminate the hypothesis P. Normally this is done using the Deduction (meta)Theorem, which looks at the microscopic steps of the deduction and usually doubles or triples the number of these microscopic steps for each hypothesis that is eliminated. We will look at a special case of this problem, without appealing to the Deduction Theorem. We assume ZF with class notation. A and B are arbitrary (possibly proper) classes. P, Q, R, S and T are wffs. We define the conditional operator, if(P, A, B), as follows: if(P, A, B) =def= { x | (x \in A & P) v (x \in B & -. P) } (where x does not occur in A, B, or P). Lemma 1. A = if(P, A, B) -> (P <-> R), B = if(P, A, B) -> (S <-> R), S |- R Proof: Logic and Axiom of Extensionality. Lemma 2. A = if(P, A, B) -> (Q <-> T), T |- P -> Q Proof: Logic and Axiom of Extensionality. Here's a simple example that illustrates how it works. Suppose we have a deduction Ord A |- Tr A which means, "Assume A is an ordinal class. Then A is a transitive class." Note that A is a class variable that may be substituted with any class expression, so this is really a deduction scheme. We want to convert this to a proof of the theorem (scheme) |- Ord A -> Tr A. The catch is that we must be able to prove "Ord A" for at least one object A (and this is what makes it weaker than the ordinary Deduction Theorem). However, it is easy to prove |- Ord 0 (the empty set is ordinal). (For a typical textbook "theorem," i.e. deduction, there is usually at least one object satisfying each hypothesis, otherwise the theorem would not be very useful. We can always go back to the standard Deduction Theorem for those hypotheses where this is not the case.) Continuing with the example: Equality axioms (and Extensionality) yield |- A = if(Ord A, A, 0) -> (Ord A <-> Ord if(Ord A, A, 0)) (1) |- 0 = if(Ord A, A, 0) -> (Ord 0 <-> Ord if(Ord A, A, 0)) (2) From (1), (2) and |- Ord 0, Lemma 1 yields |- Ord if(Ord A, A, 0) (3) From (3) and substituting if(Ord A, A, 0) for A in the original deduction, |- Tr if(Ord A, A, 0) (4) Equality axioms (and Extensionality) yield |- A = if(Ord A, A, 0) -> (Tr A <-> Tr if(Ord A, A, 0)) (5) From (4) and (5), Lemma 2 yields |- Ord A -> Tr A (Q.E.D.) | ||
Syntax | cif 4086 | Extend class notation to include the conditional operator. See df-if 4087 for a description. (In older databases this was denoted "ded".) |
class if(𝜑, 𝐴, 𝐵) | ||
Definition | df-if 4087* |
Define the conditional operator. Read if(𝜑, 𝐴, 𝐵) as "if
𝜑 then 𝐴 else 𝐵."
See iftrue 4092 and iffalse 4095 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 older versions of this database, this
operator was denoted "ded" and called the "deduction
class.")
An important use for us is in conjunction with the weak deduction theorem, which converts a hypothesis into an antecedent. In that role, 𝐴 is a class variable in the hypothesis and 𝐵 is a class (usually a constant) that makes the hypothesis true when it is substituted for 𝐴. See dedth 4139 for the main part of the weak deduction theorem, elimhyp 4146 to eliminate a hypothesis, and keephyp 4152 to keep a hypothesis. See the Deduction Theorem link on the Metamath Proof Explorer Home Page for a description of the weak deduction theorem. (Contributed by NM, 15-May-1999.) |
⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))} | ||
Theorem | dfif2 4088* | An alternate definition of the conditional operator df-if 4087 with one fewer connectives (but probably less intuitive to understand). (Contributed by NM, 30-Jan-2006.) |
⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜑))} | ||
Theorem | dfif6 4089* | An alternate definition of the conditional operator df-if 4087 as a simple class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.) |
⊢ if(𝜑, 𝐴, 𝐵) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ ¬ 𝜑}) | ||
Theorem | ifeq1 4090 | Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 = 𝐵 → if(𝜑, 𝐴, 𝐶) = if(𝜑, 𝐵, 𝐶)) | ||
Theorem | ifeq2 4091 | Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 = 𝐵 → if(𝜑, 𝐶, 𝐴) = if(𝜑, 𝐶, 𝐵)) | ||
Theorem | iftrue 4092 | 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 4093 | Inference associated with iftrue 4092. (Contributed by BJ, 7-Oct-2018.) |
⊢ 𝜑 ⇒ ⊢ if(𝜑, 𝐴, 𝐵) = 𝐴 | ||
Theorem | iftrued 4094 | Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐴) | ||
Theorem | iffalse 4095 | Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.) |
⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | ||
Theorem | iffalsei 4096 | Inference associated with iffalse 4095. (Contributed by BJ, 7-Oct-2018.) |
⊢ ¬ 𝜑 ⇒ ⊢ if(𝜑, 𝐴, 𝐵) = 𝐵 | ||
Theorem | iffalsed 4097 | Value of the conditional operator when its first argument is false. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = 𝐵) | ||
Theorem | ifnefalse 4098 | 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 4095 directly in this case. It happens, e.g., in oevn0 7595. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷) | ||
Theorem | ifsb 4099 | Distribute a function over an if-clause. (Contributed by Mario Carneiro, 14-Aug-2013.) |
⊢ (if(𝜑, 𝐴, 𝐵) = 𝐴 → 𝐶 = 𝐷) & ⊢ (if(𝜑, 𝐴, 𝐵) = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ 𝐶 = if(𝜑, 𝐷, 𝐸) | ||
Theorem | dfif3 4100* | Alternate definition of the conditional operator df-if 4087. 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 ∖ 𝐶))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |