Home | Metamath
Proof Explorer Theorem List (p. 49 of 449) | < 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | opeq1d 4801 | Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) | ||
Theorem | opeq2d 4802 | Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉) | ||
Theorem | opeq12d 4803 | Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐷〉) | ||
Theorem | oteq1 4804 | Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.) |
⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶, 𝐷〉 = 〈𝐵, 𝐶, 𝐷〉) | ||
Theorem | oteq2 4805 | Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.) |
⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐴, 𝐷〉 = 〈𝐶, 𝐵, 𝐷〉) | ||
Theorem | oteq3 4806 | Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.) |
⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐷, 𝐴〉 = 〈𝐶, 𝐷, 𝐵〉) | ||
Theorem | oteq1d 4807 | Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐶, 𝐷〉 = 〈𝐵, 𝐶, 𝐷〉) | ||
Theorem | oteq2d 4808 | Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐴, 𝐷〉 = 〈𝐶, 𝐵, 𝐷〉) | ||
Theorem | oteq3d 4809 | Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐷, 𝐴〉 = 〈𝐶, 𝐷, 𝐵〉) | ||
Theorem | oteq123d 4810 | Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) & ⊢ (𝜑 → 𝐸 = 𝐹) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐶, 𝐸〉 = 〈𝐵, 𝐷, 𝐹〉) | ||
Theorem | nfop 4811 | Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥〈𝐴, 𝐵〉 | ||
Theorem | nfopd 4812 | Deduction version of bound-variable hypothesis builder nfop 4811. This shows how the deduction version of a not-free theorem such as nfop 4811 can be created from the corresponding not-free inference theorem. (Contributed by NM, 4-Feb-2008.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥〈𝐴, 𝐵〉) | ||
Theorem | csbopg 4813 | Distribution of class substitution over ordered pairs. (Contributed by Drahflow, 25-Sep-2015.) (Revised by Mario Carneiro, 29-Oct-2015.) (Revised by ML, 25-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌〈𝐶, 𝐷〉 = 〈⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷〉) | ||
Theorem | opidg 4814 | The ordered pair 〈𝐴, 𝐴〉 in Kuratowski's representation. Closed form of opid 4815. (Contributed by Peter Mazsa, 22-Jul-2019.) (Avoid depending on this detail.) |
⊢ (𝐴 ∈ 𝑉 → 〈𝐴, 𝐴〉 = {{𝐴}}) | ||
Theorem | opid 4815 | The ordered pair 〈𝐴, 𝐴〉 in Kuratowski's representation. Inference form of opidg 4814. (Contributed by FL, 28-Dec-2011.) (Proof shortened by AV, 16-Feb-2022.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 〈𝐴, 𝐴〉 = {{𝐴}} | ||
Theorem | ralunsn 4816* | Restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro, 23-Apr-2015.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))) | ||
Theorem | 2ralunsn 4817* | Double restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝐵 ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∪ {𝐵})∀𝑦 ∈ (𝐴 ∪ {𝐵})𝜑 ↔ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) ∧ (∀𝑦 ∈ 𝐴 𝜒 ∧ 𝜃)))) | ||
Theorem | opprc 4818 | Expansion of an ordered pair when either member is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → 〈𝐴, 𝐵〉 = ∅) | ||
Theorem | opprc1 4819 | Expansion of an ordered pair when the first member is a proper class. See also opprc 4818. (Contributed by NM, 10-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (¬ 𝐴 ∈ V → 〈𝐴, 𝐵〉 = ∅) | ||
Theorem | opprc2 4820 | Expansion of an ordered pair when the second member is a proper class. See also opprc 4818. (Contributed by NM, 15-Nov-1994.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (¬ 𝐵 ∈ V → 〈𝐴, 𝐵〉 = ∅) | ||
Theorem | oprcl 4821 | If an ordered pair has an element, then its arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐶 ∈ 〈𝐴, 𝐵〉 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | pwsn 4822 | The power set of a singleton. (Contributed by NM, 5-Jun-2006.) |
⊢ 𝒫 {𝐴} = {∅, {𝐴}} | ||
Theorem | pwsnALT 4823 | Alternate proof of pwsn 4822, more direct. (Contributed by NM, 5-Jun-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝒫 {𝐴} = {∅, {𝐴}} | ||
Theorem | pwpr 4824 | The power set of an unordered pair. (Contributed by NM, 1-May-2009.) |
⊢ 𝒫 {𝐴, 𝐵} = ({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}}) | ||
Theorem | pwtp 4825 | The power set of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016.) |
⊢ 𝒫 {𝐴, 𝐵, 𝐶} = (({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}}) ∪ ({{𝐶}, {𝐴, 𝐶}} ∪ {{𝐵, 𝐶}, {𝐴, 𝐵, 𝐶}})) | ||
Theorem | pwpwpw0 4826 | Compute the power set of the power set of the power set of the empty set. (See also pw0 4737 and pwpw0 4738.) (Contributed by NM, 2-May-2009.) |
⊢ 𝒫 {∅, {∅}} = ({∅, {∅}} ∪ {{{∅}}, {∅, {∅}}}) | ||
Theorem | pwv 4827 |
The power class of the universe is the universe. Exercise 4.12(d) of
[Mendelson] p. 235.
The collection of all classes is of course larger than V, which is the collection of all sets. But 𝒫 V, being a class, cannot contain proper classes, so 𝒫 V is actually no larger than V. This fact is exploited in ncanth 7101. (Contributed by NM, 14-Sep-2003.) |
⊢ 𝒫 V = V | ||
Theorem | prproe 4828* | For an element of a proper unordered pair of elements of a class 𝑉, there is another (different) element of the class 𝑉 which is an element of the proper pair. (Contributed by AV, 18-Dec-2021.) |
⊢ ((𝐶 ∈ {𝐴, 𝐵} ∧ 𝐴 ≠ 𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ∃𝑣 ∈ (𝑉 ∖ {𝐶})𝑣 ∈ {𝐴, 𝐵}) | ||
Theorem | 3elpr2eq 4829 | If there are three elements in a proper unordered pair, and two of them are different from the third one, the two must be equal. (Contributed by AV, 19-Dec-2021.) |
⊢ (((𝑋 ∈ {𝐴, 𝐵} ∧ 𝑌 ∈ {𝐴, 𝐵} ∧ 𝑍 ∈ {𝐴, 𝐵}) ∧ (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋)) → 𝑌 = 𝑍) | ||
Syntax | cuni 4830 | Extend class notation to include the union of a class. Read: "union (of) 𝐴". |
class ∪ 𝐴 | ||
Definition | df-uni 4831* | Define the union of a class i.e. the collection of all members of the members of the class. Definition 5.5 of [TakeutiZaring] p. 16. For example, ∪ {{1, 3}, {1, 8}} = {1, 3, 8} (ex-uni 28132). This is similar to the union of two classes df-un 3938. (Contributed by NM, 23-Aug-1993.) |
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)} | ||
Theorem | dfuni2 4832* | Alternate definition of class union. (Contributed by NM, 28-Jun-1998.) |
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} | ||
Theorem | eluni 4833* | Membership in class union. (Contributed by NM, 22-May-1994.) |
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)) | ||
Theorem | eluni2 4834* | Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.) |
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) | ||
Theorem | elunii 4835 | Membership in class union. (Contributed by NM, 24-Mar-1995.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶) | ||
Theorem | nfunid 4836 | Deduction version of nfuni 4837. (Contributed by NM, 18-Feb-2013.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴) | ||
Theorem | nfuni 4837 | Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥∪ 𝐴 | ||
Theorem | unieq 4838 | Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18. (Contributed by NM, 10-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | ||
Theorem | unieqi 4839 | Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∪ 𝐴 = ∪ 𝐵 | ||
Theorem | unieqd 4840 | Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵) | ||
Theorem | eluniab 4841* | Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑)) | ||
Theorem | elunirab 4842* | Membership in union of a class abstraction. (Contributed by NM, 4-Oct-2006.) |
⊢ (𝐴 ∈ ∪ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝜑)) | ||
Theorem | unipr 4843 | The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 23-Aug-1993.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵) | ||
Theorem | uniprg 4844 | The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 25-Aug-2006.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)) | ||
Theorem | unisng 4845 | A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 13-Aug-2002.) |
⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴) | ||
Theorem | unisn 4846 | A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∪ {𝐴} = 𝐴 | ||
Theorem | unisn3 4847* | Union of a singleton in the form of a restricted class abstraction. (Contributed by NM, 3-Jul-2008.) |
⊢ (𝐴 ∈ 𝐵 → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 = 𝐴} = 𝐴) | ||
Theorem | dfnfc2 4848* | An alternative statement of the effective freeness of a class 𝐴, when it is a set. (Contributed by Mario Carneiro, 14-Oct-2016.) (Proof shortened by JJ, 26-Jul-2021.) |
⊢ (∀𝑥 𝐴 ∈ 𝑉 → (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴)) | ||
Theorem | uniun 4849 | The class union of the union of two classes. Theorem 8.3 of [Quine] p. 53. (Contributed by NM, 20-Aug-1993.) |
⊢ ∪ (𝐴 ∪ 𝐵) = (∪ 𝐴 ∪ ∪ 𝐵) | ||
Theorem | uniin 4850 | The class union of the intersection of two classes. Exercise 4.12(n) of [Mendelson] p. 235. See uniinqs 8366 for a condition where equality holds. (Contributed by NM, 4-Dec-2003.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ ∪ (𝐴 ∩ 𝐵) ⊆ (∪ 𝐴 ∩ ∪ 𝐵) | ||
Theorem | uniss 4851 | Subclass relationship for class union. Theorem 61 of [Suppes] p. 39. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵) | ||
Theorem | ssuni 4852 | Subclass relationship for class union. (Contributed by NM, 24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 26-Jul-2021.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ⊆ ∪ 𝐶) | ||
Theorem | unissi 4853 | Subclass relationship for subclass union. Inference form of uniss 4851. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ∪ 𝐴 ⊆ ∪ 𝐵 | ||
Theorem | unissd 4854 | Subclass relationship for subclass union. Deduction form of uniss 4851. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵) | ||
Theorem | uni0b 4855 | The union of a set is empty iff the set is included in the singleton of the empty set. (Contributed by NM, 12-Sep-2004.) |
⊢ (∪ 𝐴 = ∅ ↔ 𝐴 ⊆ {∅}) | ||
Theorem | uni0c 4856* | The union of a set is empty iff all of its members are empty. (Contributed by NM, 16-Aug-2006.) |
⊢ (∪ 𝐴 = ∅ ↔ ∀𝑥 ∈ 𝐴 𝑥 = ∅) | ||
Theorem | uni0 4857 | The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul 5201 by Eric Schmidt.) (Contributed by NM, 16-Sep-1993.) (Revised by Eric Schmidt, 4-Apr-2007.) |
⊢ ∪ ∅ = ∅ | ||
Theorem | csbuni 4858 | Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012.) (Revised by NM, 22-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌∪ 𝐵 = ∪ ⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | elssuni 4859 | An element of a class is a subclass of its union. Theorem 8.6 of [Quine] p. 54. Also the basis for Proposition 7.20 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Jun-1994.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ⊆ ∪ 𝐵) | ||
Theorem | unissel 4860 | Condition turning a subclass relationship for union into an equality. (Contributed by NM, 18-Jul-2006.) |
⊢ ((∪ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐴) → ∪ 𝐴 = 𝐵) | ||
Theorem | unissb 4861* | Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.) |
⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) | ||
Theorem | uniss2 4862* | A subclass condition on the members of two classes that implies a subclass relation on their unions. Proposition 8.6 of [TakeutiZaring] p. 59. See iunss2 4964 for a generalization to indexed unions. (Contributed by NM, 22-Mar-2004.) |
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∪ 𝐴 ⊆ ∪ 𝐵) | ||
Theorem | unidif 4863* | If the difference 𝐴 ∖ 𝐵 contains the largest members of 𝐴, then the union of the difference is the union of 𝐴. (Contributed by NM, 22-Mar-2004.) |
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ (𝐴 ∖ 𝐵)𝑥 ⊆ 𝑦 → ∪ (𝐴 ∖ 𝐵) = ∪ 𝐴) | ||
Theorem | ssunieq 4864* | Relationship implying union. (Contributed by NM, 10-Nov-1999.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝑥 ⊆ 𝐴) → 𝐴 = ∪ 𝐵) | ||
Theorem | unimax 4865* | Any member of a class is the largest of those members that it includes. (Contributed by NM, 13-Aug-2002.) |
⊢ (𝐴 ∈ 𝐵 → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} = 𝐴) | ||
Theorem | pwuni 4866 | A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.) |
⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴 | ||
Syntax | cint 4867 | Extend class notation to include the intersection of a class. Read: "intersection (of) 𝐴". |
class ∩ 𝐴 | ||
Definition | df-int 4868* | Define the intersection of a class. Definition 7.35 of [TakeutiZaring] p. 44. For example, ∩ {{1, 3}, {1, 8}} = {1}. Compare this with the intersection of two classes, df-in 3940. (Contributed by NM, 18-Aug-1993.) |
⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦)} | ||
Theorem | dfint2 4869* | Alternate definition of class intersection. (Contributed by NM, 28-Jun-1998.) |
⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} | ||
Theorem | inteq 4870 | Equality law for intersection. (Contributed by NM, 13-Sep-1999.) |
⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵) | ||
Theorem | inteqi 4871 | Equality inference for class intersection. (Contributed by NM, 2-Sep-2003.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∩ 𝐴 = ∩ 𝐵 | ||
Theorem | inteqd 4872 | Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵) | ||
Theorem | elint 4873* | Membership in class intersection. (Contributed by NM, 21-May-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥)) | ||
Theorem | elint2 4874* | Membership in class intersection. (Contributed by NM, 14-Oct-1999.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) | ||
Theorem | elintg 4875* | Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003.) (Proof shortened by JJ, 26-Jul-2021.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)) | ||
Theorem | elinti 4876 | Membership in class intersection. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (𝐴 ∈ ∩ 𝐵 → (𝐶 ∈ 𝐵 → 𝐴 ∈ 𝐶)) | ||
Theorem | nfint 4877 | Bound-variable hypothesis builder for intersection. (Contributed by NM, 2-Feb-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥∩ 𝐴 | ||
Theorem | elintab 4878* | Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)) | ||
Theorem | elintrab 4879* | Membership in the intersection of a class abstraction. (Contributed by NM, 17-Oct-1999.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥)) | ||
Theorem | elintrabg 4880* | Membership in the intersection of a class abstraction. (Contributed by NM, 17-Feb-2007.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥))) | ||
Theorem | int0 4881 | The intersection of the empty set is the universal class. Exercise 2 of [TakeutiZaring] p. 44. (Contributed by NM, 18-Aug-1993.) (Proof shortened by JJ, 26-Jul-2021.) |
⊢ ∩ ∅ = V | ||
Theorem | intss1 4882 | An element of a class includes the intersection of the class. Exercise 4 of [TakeutiZaring] p. 44 (with correction), generalized to classes. (Contributed by NM, 18-Nov-1995.) |
⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴) | ||
Theorem | ssint 4883* | Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52 and its converse. (Contributed by NM, 14-Oct-1999.) |
⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥) | ||
Theorem | ssintab 4884* | Subclass of the intersection of a class abstraction. (Contributed by NM, 31-Jul-2006.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (𝐴 ⊆ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ⊆ 𝑥)) | ||
Theorem | ssintub 4885* | Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.) |
⊢ 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} | ||
Theorem | ssmin 4886* | Subclass of the minimum value of class of supersets. (Contributed by NM, 10-Aug-2006.) |
⊢ 𝐴 ⊆ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)} | ||
Theorem | intmin 4887* | Any member of a class is the smallest of those members that include it. (Contributed by NM, 13-Aug-2002.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (𝐴 ∈ 𝐵 → ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} = 𝐴) | ||
Theorem | intss 4888 | Intersection of subclasses. (Contributed by NM, 14-Oct-1999.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ (𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴) | ||
Theorem | intssuni 4889 | The intersection of a nonempty set is a subclass of its union. (Contributed by NM, 29-Jul-2006.) |
⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴) | ||
Theorem | ssintrab 4890* | Subclass of the intersection of a restricted class builder. (Contributed by NM, 30-Jan-2015.) |
⊢ (𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ⊆ 𝑥)) | ||
Theorem | unissint 4891 | If the union of a class is included in its intersection, the class is either the empty set or a singleton (uniintsn 4904). (Contributed by NM, 30-Oct-2010.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (∪ 𝐴 ⊆ ∩ 𝐴 ↔ (𝐴 = ∅ ∨ ∪ 𝐴 = ∩ 𝐴)) | ||
Theorem | intssuni2 4892 | Subclass relationship for intersection and union. (Contributed by NM, 29-Jul-2006.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ⊆ ∪ 𝐵) | ||
Theorem | intminss 4893* | Under subset ordering, the intersection of a restricted class abstraction is less than or equal to any of its members. (Contributed by NM, 7-Sep-2013.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ⊆ 𝐴) | ||
Theorem | intmin2 4894* | Any set is the smallest of all sets that include it. (Contributed by NM, 20-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∩ {𝑥 ∣ 𝐴 ⊆ 𝑥} = 𝐴 | ||
Theorem | intmin3 4895* | Under subset ordering, the intersection of a class abstraction is less than or equal to any of its members. (Contributed by NM, 3-Jul-2005.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ (𝐴 ∈ 𝑉 → ∩ {𝑥 ∣ 𝜑} ⊆ 𝐴) | ||
Theorem | intmin4 4896* | Elimination of a conjunct in a class intersection. (Contributed by NM, 31-Jul-2006.) |
⊢ (𝐴 ⊆ ∩ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)} = ∩ {𝑥 ∣ 𝜑}) | ||
Theorem | intab 4897* | The intersection of a special case of a class abstraction. 𝑦 may be free in 𝜑 and 𝐴, which can be thought of a 𝜑(𝑦) and 𝐴(𝑦). Typically, abrexex2 7659 or abexssex 7660 can be used to satisfy the second hypothesis. (Contributed by NM, 28-Jul-2006.) (Proof shortened by Mario Carneiro, 14-Nov-2016.) |
⊢ 𝐴 ∈ V & ⊢ {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} ∈ V ⇒ ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} | ||
Theorem | int0el 4898 | The intersection of a class containing the empty set is empty. (Contributed by NM, 24-Apr-2004.) |
⊢ (∅ ∈ 𝐴 → ∩ 𝐴 = ∅) | ||
Theorem | intun 4899 | The class intersection of the union of two classes. Theorem 78 of [Suppes] p. 42. (Contributed by NM, 22-Sep-2002.) |
⊢ ∩ (𝐴 ∪ 𝐵) = (∩ 𝐴 ∩ ∩ 𝐵) | ||
Theorem | intpr 4900 | The intersection of a pair is the intersection of its members. Theorem 71 of [Suppes] p. 42. (Contributed by NM, 14-Oct-1999.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |