| Metamath
Proof Explorer Theorem List (p. 42 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | pssned 4101 | Proper subclasses are unequal. Deduction form of pssne 4099. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ⊊ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
| Theorem | sspss 4102 | Subclass in terms of proper subclass. (Contributed by NM, 25-Feb-1996.) |
| ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵)) | ||
| Theorem | pssirr 4103 | Proper subclass is irreflexive. Theorem 7 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) |
| ⊢ ¬ 𝐴 ⊊ 𝐴 | ||
| Theorem | pssn2lp 4104 | Proper subclass has no 2-cycle loops. Compare Theorem 8 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ ¬ (𝐴 ⊊ 𝐵 ∧ 𝐵 ⊊ 𝐴) | ||
| Theorem | sspsstri 4105 | Two ways of stating trichotomy with respect to inclusion. (Contributed by NM, 12-Aug-2004.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴)) | ||
| Theorem | ssnpss 4106 | Partial trichotomy law for subclasses. (Contributed by NM, 16-May-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ (𝐴 ⊆ 𝐵 → ¬ 𝐵 ⊊ 𝐴) | ||
| Theorem | psstr 4107 | Transitive law for proper subclass. Theorem 9 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) |
| ⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊊ 𝐶) → 𝐴 ⊊ 𝐶) | ||
| Theorem | sspsstr 4108 | Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊊ 𝐶) → 𝐴 ⊊ 𝐶) | ||
| Theorem | psssstr 4109 | Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996.) |
| ⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊊ 𝐶) | ||
| Theorem | psstrd 4110 | Proper subclass inclusion is transitive. Deduction form of psstr 4107. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ⊊ 𝐵) & ⊢ (𝜑 → 𝐵 ⊊ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊊ 𝐶) | ||
| Theorem | sspsstrd 4111 | Transitivity involving subclass and proper subclass inclusion. Deduction form of sspsstr 4108. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊊ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊊ 𝐶) | ||
| Theorem | psssstrd 4112 | Transitivity involving subclass and proper subclass inclusion. Deduction form of psssstr 4109. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ⊊ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊊ 𝐶) | ||
| Theorem | npss 4113 | A class is not a proper subclass of another iff it satisfies a one-directional form of eqss 3999. (Contributed by Mario Carneiro, 15-May-2015.) |
| ⊢ (¬ 𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 → 𝐴 = 𝐵)) | ||
| Theorem | ssnelpss 4114 | A subclass missing a member is a proper subclass. (Contributed by NM, 12-Jan-2002.) |
| ⊢ (𝐴 ⊆ 𝐵 → ((𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴) → 𝐴 ⊊ 𝐵)) | ||
| Theorem | ssnelpssd 4115 | Subclass inclusion with one element of the superclass missing is proper subclass inclusion. Deduction form of ssnelpss 4114. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ⊊ 𝐵) | ||
| Theorem | ssexnelpss 4116* | If there is an element of a class which is not contained in a subclass, the subclass is a proper subclass. (Contributed by AV, 29-Jan-2020.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝑥 ∉ 𝐴) → 𝐴 ⊊ 𝐵) | ||
| Theorem | dfdif3 4117* | Alternate definition of class difference. (Contributed by BJ and Jim Kingdon, 16-Jun-2022.) (Proof shortened by SN, 15-Aug-2025.) |
| ⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 𝑥 ≠ 𝑦} | ||
| Theorem | dfdif3OLD 4118* | Obsolete version of dfdif3 4117 as of 15-Aug-2025. (Contributed by BJ and Jim Kingdon, 16-Jun-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ∖ 𝐵) = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐵 𝑥 ≠ 𝑦} | ||
| Theorem | difeq1 4119 | Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) | ||
| Theorem | difeq2 4120 | Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)) | ||
| Theorem | difeq12 4121 | Equality theorem for class difference. (Contributed by FL, 31-Aug-2009.) |
| ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)) | ||
| Theorem | difeq1i 4122 | Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶) | ||
| Theorem | difeq2i 4123 | Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵) | ||
| Theorem | difeq12i 4124 | Equality inference for class difference. (Contributed by NM, 29-Aug-2004.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷) | ||
| Theorem | difeq1d 4125 | Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) | ||
| Theorem | difeq2d 4126 | Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)) | ||
| Theorem | difeq12d 4127 | Equality deduction for class difference. (Contributed by FL, 29-May-2014.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)) | ||
| Theorem | difeqri 4128* | Inference from membership to difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ⇒ ⊢ (𝐴 ∖ 𝐵) = 𝐶 | ||
| Theorem | nfdif 4129 | Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) Avoid ax-10 2141, ax-11 2157, ax-12 2177. (Revised by SN, 14-May-2025.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵) | ||
| Theorem | nfdifOLD 4130 | Obsolete version of nfdif 4129 as of 14-May-2025. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵) | ||
| Theorem | eldifi 4131 | Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.) |
| ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ 𝐵) | ||
| Theorem | eldifn 4132 | Implication of membership in a class difference. (Contributed by NM, 3-May-1994.) |
| ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → ¬ 𝐴 ∈ 𝐶) | ||
| Theorem | elndif 4133 | A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994.) |
| ⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ 𝐵)) | ||
| Theorem | neldif 4134 | Implication of membership in a class difference. (Contributed by NM, 28-Jun-1994.) |
| ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ (𝐵 ∖ 𝐶)) → 𝐴 ∈ 𝐶) | ||
| Theorem | difdif 4135 | Double class difference. Exercise 11 of [TakeutiZaring] p. 22. (Contributed by NM, 17-May-1998.) |
| ⊢ (𝐴 ∖ (𝐵 ∖ 𝐴)) = 𝐴 | ||
| Theorem | difss 4136 | Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.) |
| ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴 | ||
| Theorem | difssd 4137 | A difference of two classes is contained in the minuend. Deduction form of difss 4136. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐴) | ||
| Theorem | difss2 4138 | If a class is contained in a difference, it is contained in the minuend. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝐴 ⊆ (𝐵 ∖ 𝐶) → 𝐴 ⊆ 𝐵) | ||
| Theorem | difss2d 4139 | If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 4138. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∖ 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
| Theorem | ssdifss 4140 | Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.) |
| ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ 𝐵) | ||
| Theorem | ddif 4141 | Double complement under universal class. Exercise 4.10(s) of [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.) |
| ⊢ (V ∖ (V ∖ 𝐴)) = 𝐴 | ||
| Theorem | ssconb 4142 | Contraposition law for subsets. (Contributed by NM, 22-Mar-1998.) |
| ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ⊆ (𝐶 ∖ 𝐵) ↔ 𝐵 ⊆ (𝐶 ∖ 𝐴))) | ||
| Theorem | sscon 4143 | Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.) |
| ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)) | ||
| Theorem | ssdif 4144 | Difference law for subsets. (Contributed by NM, 28-May-1998.) |
| ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) | ||
| Theorem | ssdifd 4145 | If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is contained in (𝐵 ∖ 𝐶). Deduction form of ssdif 4144. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) | ||
| Theorem | sscond 4146 | If 𝐴 is contained in 𝐵, then (𝐶 ∖ 𝐵) is contained in (𝐶 ∖ 𝐴). Deduction form of sscon 4143. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)) | ||
| Theorem | ssdifssd 4147 | If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is also contained in 𝐵. Deduction form of ssdifss 4140. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ 𝐵) | ||
| Theorem | ssdif2d 4148 | If 𝐴 is contained in 𝐵 and 𝐶 is contained in 𝐷, then (𝐴 ∖ 𝐷) is contained in (𝐵 ∖ 𝐶). Deduction form. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐷) ⊆ (𝐵 ∖ 𝐶)) | ||
| Theorem | raldifb 4149 | Restricted universal quantification on a class difference in terms of an implication. (Contributed by Alexander van der Vekens, 3-Jan-2018.) |
| ⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∉ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ (𝐴 ∖ 𝐵)𝜑) | ||
| Theorem | rexdifi 4150 | Restricted existential quantification over a difference. (Contributed by AV, 25-Oct-2023.) |
| ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝜑) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)𝜑) | ||
| Theorem | complss 4151 | Complementation reverses inclusion. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 19-Mar-2021.) |
| ⊢ (𝐴 ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ (V ∖ 𝐴)) | ||
| Theorem | compleq 4152 | Two classes are equal if and only if their complements are equal. (Contributed by BJ, 19-Mar-2021.) |
| ⊢ (𝐴 = 𝐵 ↔ (V ∖ 𝐴) = (V ∖ 𝐵)) | ||
| Theorem | elun 4153 | Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.) |
| ⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)) | ||
| Theorem | elunnel1 4154 | A member of a union that is not a member of the first class, is a member of the second class. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ ((𝐴 ∈ (𝐵 ∪ 𝐶) ∧ ¬ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐶) | ||
| Theorem | elunnel2 4155 | A member of a union that is not a member of the second class, is a member of the first class. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ ((𝐴 ∈ (𝐵 ∪ 𝐶) ∧ ¬ 𝐴 ∈ 𝐶) → 𝐴 ∈ 𝐵) | ||
| Theorem | uneqri 4156* | Inference from membership to union. (Contributed by NM, 21-Jun-1993.) |
| ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ⇒ ⊢ (𝐴 ∪ 𝐵) = 𝐶 | ||
| Theorem | unidm 4157 | Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 21-Jun-1993.) |
| ⊢ (𝐴 ∪ 𝐴) = 𝐴 | ||
| Theorem | uncom 4158 | Commutative law for union of classes. Exercise 6 of [TakeutiZaring] p. 17. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴) | ||
| Theorem | equncom 4159 | If a class equals the union of two other classes, then it equals the union of those two classes commuted. equncom 4159 was automatically derived from equncomVD 44888 using the tools program translate_without_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.) |
| ⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵)) | ||
| Theorem | equncomi 4160 | Inference form of equncom 4159. equncomi 4160 was automatically derived from equncomiVD 44889 using the tools program translate_without_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.) |
| ⊢ 𝐴 = (𝐵 ∪ 𝐶) ⇒ ⊢ 𝐴 = (𝐶 ∪ 𝐵) | ||
| Theorem | uneq1 4161 | Equality theorem for the union of two classes. (Contributed by NM, 15-Jul-1993.) |
| ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | ||
| Theorem | uneq2 4162 | Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.) |
| ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)) | ||
| Theorem | uneq12 4163 | Equality theorem for the union of two classes. (Contributed by NM, 29-Mar-1998.) |
| ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) | ||
| Theorem | uneq1i 4164 | Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶) | ||
| Theorem | uneq2i 4165 | Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵) | ||
| Theorem | uneq12i 4166 | Equality inference for the union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷) | ||
| Theorem | uneq1d 4167 | Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | ||
| Theorem | uneq2d 4168 | Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)) | ||
| Theorem | uneq12d 4169 | Equality deduction for the union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) | ||
| Theorem | nfun 4170 | Bound-variable hypothesis builder for the union of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) Avoid ax-10 2141, ax-11 2157, ax-12 2177. (Revised by SN, 14-May-2025.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵) | ||
| Theorem | nfunOLD 4171 | Obsolete version of nfun 4170 as of 14-May-2025. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵) | ||
| Theorem | unass 4172 | Associative law for union of classes. Exercise 8 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = (𝐴 ∪ (𝐵 ∪ 𝐶)) | ||
| Theorem | un12 4173 | A rearrangement of union. (Contributed by NM, 12-Aug-2004.) |
| ⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = (𝐵 ∪ (𝐴 ∪ 𝐶)) | ||
| Theorem | un23 4174 | A rearrangement of union. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ 𝐵) | ||
| Theorem | un4 4175 | A rearrangement of the union of 4 classes. (Contributed by NM, 12-Aug-2004.) |
| ⊢ ((𝐴 ∪ 𝐵) ∪ (𝐶 ∪ 𝐷)) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐷)) | ||
| Theorem | unundi 4176 | Union distributes over itself. (Contributed by NM, 17-Aug-2004.) |
| ⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = ((𝐴 ∪ 𝐵) ∪ (𝐴 ∪ 𝐶)) | ||
| Theorem | unundir 4177 | Union distributes over itself. (Contributed by NM, 17-Aug-2004.) |
| ⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐶)) | ||
| Theorem | ssun1 4178 | Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.) |
| ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) | ||
| Theorem | ssun2 4179 | Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.) |
| ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴) | ||
| Theorem | ssun3 4180 | Subclass law for union of classes. (Contributed by NM, 5-Aug-1993.) |
| ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐵 ∪ 𝐶)) | ||
| Theorem | ssun4 4181 | Subclass law for union of classes. (Contributed by NM, 14-Aug-1994.) |
| ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐶 ∪ 𝐵)) | ||
| Theorem | elun1 4182 | Membership law for union of classes. (Contributed by NM, 5-Aug-1993.) |
| ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶)) | ||
| Theorem | elun2 4183 | Membership law for union of classes. (Contributed by NM, 30-Aug-1993.) |
| ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵)) | ||
| Theorem | elunant 4184 | A statement is true for every element of the union of a pair of classes if and only if it is true for every element of the first class and for every element of the second class. (Contributed by BTernaryTau, 27-Sep-2023.) |
| ⊢ ((𝐶 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝐶 ∈ 𝐴 → 𝜑) ∧ (𝐶 ∈ 𝐵 → 𝜑))) | ||
| Theorem | unss1 4185 | Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶)) | ||
| Theorem | ssequn1 4186 | A relationship between subclass and union. Theorem 26 of [Suppes] p. 27. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) | ||
| Theorem | unss2 4187 | Subclass law for union of classes. Exercise 7 of [TakeutiZaring] p. 18. (Contributed by NM, 14-Oct-1999.) |
| ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∪ 𝐴) ⊆ (𝐶 ∪ 𝐵)) | ||
| Theorem | unss12 4188 | Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷)) | ||
| Theorem | ssequn2 4189 | A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.) |
| ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵) | ||
| Theorem | unss 4190 | The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27 and its converse. (Contributed by NM, 11-Jun-2004.) |
| ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) | ||
| Theorem | unssi 4191 | An inference showing the union of two subclasses is a subclass. (Contributed by Raph Levien, 10-Dec-2002.) |
| ⊢ 𝐴 ⊆ 𝐶 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶 | ||
| Theorem | unssd 4192 | A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) | ||
| Theorem | unssad 4193 | If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4190. Partial converse of unssd 4192. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
| Theorem | unssbd 4194 | If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐵. One-way deduction form of unss 4190. Partial converse of unssd 4192. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | ||
| Theorem | ssun 4195 | A condition that implies inclusion in the union of two classes. (Contributed by NM, 23-Nov-2003.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶) → 𝐴 ⊆ (𝐵 ∪ 𝐶)) | ||
| Theorem | rexun 4196 | Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011.) |
| ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑)) | ||
| Theorem | ralunb 4197 | Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
| ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑)) | ||
| Theorem | ralun 4198 | Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) → ∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑) | ||
| Theorem | elini 4199 | Membership in an intersection of two classes. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ 𝐴 ∈ 𝐵 & ⊢ 𝐴 ∈ 𝐶 ⇒ ⊢ 𝐴 ∈ (𝐵 ∩ 𝐶) | ||
| Theorem | elind 4200 | Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |