Home | Metamath
Proof Explorer Theorem List (p. 51 of 465) | < 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-29266) |
Hilbert Space Explorer
(29267-30789) |
Users' Mathboxes
(30790-46477) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iunin1 5001* | Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4988 to recover Enderton's theorem. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ ∪ 𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵) = (∪ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵) | ||
Theorem | iinun2 5002* | Indexed intersection of union. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4989 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.) |
⊢ ∩ 𝑥 ∈ 𝐴 (𝐵 ∪ 𝐶) = (𝐵 ∪ ∩ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | iundif2 5003* | Indexed union of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use intiin 4989 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.) |
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (𝐵 ∖ ∩ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | iindif1 5004* | Indexed intersection of class difference with the subtrahend held constant. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (∩ 𝑥 ∈ 𝐴 𝐵 ∖ 𝐶)) | ||
Theorem | 2iunin 5005* | Rearrange indexed unions over intersection. (Contributed by NM, 18-Dec-2008.) |
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 (𝐶 ∩ 𝐷) = (∪ 𝑥 ∈ 𝐴 𝐶 ∩ ∪ 𝑦 ∈ 𝐵 𝐷) | ||
Theorem | iindif2 5006* | Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use uniiun 4988 to recover Enderton's theorem. (Contributed by NM, 5-Oct-2006.) |
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶)) | ||
Theorem | iinin2 5007* | Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4989 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶)) | ||
Theorem | iinin1 5008* | Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4989 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵) = (∩ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵)) | ||
Theorem | iinvdif 5009* | The indexed intersection of a complement. (Contributed by Gérard Lang, 5-Aug-2018.) |
⊢ ∩ 𝑥 ∈ 𝐴 (V ∖ 𝐵) = (V ∖ ∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | elriin 5010* | Elementhood in a relative intersection. (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ (𝐵 ∈ (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) ↔ (𝐵 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑆)) | ||
Theorem | riin0 5011* | Relative intersection of an empty family. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (𝑋 = ∅ → (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) = 𝐴) | ||
Theorem | riinn0 5012* | Relative intersection of a nonempty family. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ ((∀𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅) → (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) = ∩ 𝑥 ∈ 𝑋 𝑆) | ||
Theorem | riinrab 5013* | Relative intersection of a relative abstraction. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 {𝑦 ∈ 𝐴 ∣ 𝜑}) = {𝑦 ∈ 𝐴 ∣ ∀𝑥 ∈ 𝑋 𝜑} | ||
Theorem | symdif0 5014 | Symmetric difference with the empty class. The empty class is the identity element for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.) |
⊢ (𝐴 △ ∅) = 𝐴 | ||
Theorem | symdifv 5015 | The symmetric difference with the universal class is the complement. (Contributed by Scott Fenton, 24-Apr-2012.) |
⊢ (𝐴 △ V) = (V ∖ 𝐴) | ||
Theorem | symdifid 5016 | The symmetric difference of a class with itself is the empty class. (Contributed by Scott Fenton, 25-Apr-2012.) |
⊢ (𝐴 △ 𝐴) = ∅ | ||
Theorem | iinxsng 5017* | A singleton index picks out an instance of an indexed intersection's argument. (Contributed by NM, 15-Jan-2012.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∩ 𝑥 ∈ {𝐴}𝐵 = 𝐶) | ||
Theorem | iinxprg 5018* | Indexed intersection with an unordered pair index. (Contributed by NM, 25-Jan-2012.) |
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∩ 𝐸)) | ||
Theorem | iunxsng 5019* | A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶) | ||
Theorem | iunxsn 5020* | A singleton index picks out an instance of an indexed union's argument. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 25-Jun-2016.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶 | ||
Theorem | iunxsngf 5021* | A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.) (Revised by Thierry Arnoux, 2-May-2020.) Avoid ax-13 2372. (Revised by Gino Giotto, 19-May-2023.) |
⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶) | ||
Theorem | iunun 5022 | Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∪ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ ∪ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | iunxun 5023 | Separate a union in the index of an indexed union. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 = (∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | iunxdif3 5024* | An indexed union where some terms are the empty set. See iunxdif2 4983. (Contributed by Thierry Arnoux, 4-May-2020.) |
⊢ Ⅎ𝑥𝐸 ⇒ ⊢ (∀𝑥 ∈ 𝐸 𝐵 = ∅ → ∪ 𝑥 ∈ (𝐴 ∖ 𝐸)𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | iunxprg 5025* | A pair index picks out two instances of an indexed union's argument. (Contributed by Alexander van der Vekens, 2-Feb-2018.) |
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∪ 𝐸)) | ||
Theorem | iunxiun 5026* | Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016.) |
⊢ ∪ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 = ∪ 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 | ||
Theorem | iinuni 5027* | A relationship involving union and indexed intersection. Exercise 23 of [Enderton] p. 33. (Contributed by NM, 25-Nov-2003.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ (𝐴 ∪ ∩ 𝐵) = ∩ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) | ||
Theorem | iununi 5028* | A relationship involving union and indexed union. Exercise 25 of [Enderton] p. 33. (Contributed by NM, 25-Nov-2003.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ ((𝐵 = ∅ → 𝐴 = ∅) ↔ (𝐴 ∪ ∪ 𝐵) = ∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥)) | ||
Theorem | sspwuni 5029 | Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.) |
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵) | ||
Theorem | pwssb 5030* | Two ways to express a collection of subclasses. (Contributed by NM, 19-Jul-2006.) |
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) | ||
Theorem | elpwpw 5031 | Characterization of the elements of a double power class: they are exactly the sets whose union is included in that class. (Contributed by BJ, 29-Apr-2021.) |
⊢ (𝐴 ∈ 𝒫 𝒫 𝐵 ↔ (𝐴 ∈ V ∧ ∪ 𝐴 ⊆ 𝐵)) | ||
Theorem | pwpwab 5032* | The double power class written as a class abstraction: the class of sets whose union is included in the given class. (Contributed by BJ, 29-Apr-2021.) |
⊢ 𝒫 𝒫 𝐴 = {𝑥 ∣ ∪ 𝑥 ⊆ 𝐴} | ||
Theorem | pwpwssunieq 5033* | The class of sets whose union is equal to a given class is included in the double power class of that class. (Contributed by BJ, 29-Apr-2021.) |
⊢ {𝑥 ∣ ∪ 𝑥 = 𝐴} ⊆ 𝒫 𝒫 𝐴 | ||
Theorem | elpwuni 5034 | Relationship for power class and union. (Contributed by NM, 18-Jul-2006.) |
⊢ (𝐵 ∈ 𝐴 → (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 = 𝐵)) | ||
Theorem | iinpw 5035* | The power class of an intersection in terms of indexed intersection. Exercise 24(a) of [Enderton] p. 33. (Contributed by NM, 29-Nov-2003.) |
⊢ 𝒫 ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝒫 𝑥 | ||
Theorem | iunpwss 5036* | Inclusion of an indexed union of a power class in the power class of the union of its index. Part of Exercise 24(b) of [Enderton] p. 33. (Contributed by NM, 25-Nov-2003.) |
⊢ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 ⊆ 𝒫 ∪ 𝐴 | ||
Theorem | intss2 5037 | A nonempty intersection of a family of subsets of a class is included in that class. (Contributed by BJ, 7-Dec-2021.) |
⊢ (𝐴 ⊆ 𝒫 𝑋 → (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ 𝑋)) | ||
Theorem | rintn0 5038 | Relative intersection of a nonempty set. (Contributed by Stefan O'Rear, 3-Apr-2015.) (Revised by Mario Carneiro, 5-Jun-2015.) |
⊢ ((𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅) → (𝐴 ∩ ∩ 𝑋) = ∩ 𝑋) | ||
Syntax | wdisj 5039 | Extend wff notation to include the statement that a family of classes 𝐵(𝑥), for 𝑥 ∈ 𝐴, is a disjoint family. |
wff Disj 𝑥 ∈ 𝐴 𝐵 | ||
Definition | df-disj 5040* | A collection of classes 𝐵(𝑥) is disjoint when for each element 𝑦, it is in 𝐵(𝑥) for at most one 𝑥. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by NM, 16-Jun-2017.) |
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) | ||
Theorem | dfdisj2 5041* | Alternate definition for disjoint classes. (Contributed by NM, 17-Jun-2017.) |
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | ||
Theorem | disjss2 5042 | If each element of a collection is contained in a disjoint collection, the original collection is also disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (Disj 𝑥 ∈ 𝐴 𝐶 → Disj 𝑥 ∈ 𝐴 𝐵)) | ||
Theorem | disjeq2 5043 | Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑥 ∈ 𝐴 𝐶)) | ||
Theorem | disjeq2dv 5044* | Equality deduction for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑥 ∈ 𝐴 𝐶)) | ||
Theorem | disjss1 5045* | A subset of a disjoint collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶)) | ||
Theorem | disjeq1 5046* | Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝐴 = 𝐵 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)) | ||
Theorem | disjeq1d 5047* | Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)) | ||
Theorem | disjeq12d 5048* | Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷)) | ||
Theorem | cbvdisj 5049* | Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶) | ||
Theorem | cbvdisjv 5050* | Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 11-Dec-2016.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶) | ||
Theorem | nfdisjw 5051* | Bound-variable hypothesis builder for disjoint collection. Version of nfdisj 5052 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦Disj 𝑥 ∈ 𝐴 𝐵 | ||
Theorem | nfdisj 5052 | Bound-variable hypothesis builder for disjoint collection. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker nfdisjw 5051 when possible. (Contributed by Mario Carneiro, 14-Nov-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦Disj 𝑥 ∈ 𝐴 𝐵 | ||
Theorem | nfdisj1 5053 | Bound-variable hypothesis builder for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Ⅎ𝑥Disj 𝑥 ∈ 𝐴 𝐵 | ||
Theorem | disjor 5054* | Two ways to say that a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝑖 = 𝑗 → 𝐵 = 𝐶) ⇒ ⊢ (Disj 𝑖 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅)) | ||
Theorem | disjors 5055* | Two ways to say that a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) | ||
Theorem | disji2 5056* | Property of a disjoint collection: if 𝐵(𝑋) = 𝐶 and 𝐵(𝑌) = 𝐷, and 𝑋 ≠ 𝑌, then 𝐶 and 𝐷 are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) ⇒ ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝑋 ≠ 𝑌) → (𝐶 ∩ 𝐷) = ∅) | ||
Theorem | disji 5057* | Property of a disjoint collection: if 𝐵(𝑋) = 𝐶 and 𝐵(𝑌) = 𝐷 have a common element 𝑍, then 𝑋 = 𝑌. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) ⇒ ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (𝑍 ∈ 𝐶 ∧ 𝑍 ∈ 𝐷)) → 𝑋 = 𝑌) | ||
Theorem | invdisj 5058* | If there is a function 𝐶(𝑦) such that 𝐶(𝑦) = 𝑥 for all 𝑦 ∈ 𝐵(𝑥), then the sets 𝐵(𝑥) for distinct 𝑥 ∈ 𝐴 are disjoint. (Contributed by Mario Carneiro, 10-Dec-2016.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 = 𝑥 → Disj 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | invdisjrabw 5059* | Version of invdisjrab 5060 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ Disj 𝑦 ∈ 𝐴 {𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦} | ||
Theorem | invdisjrab 5060* | The restricted class abstractions {𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦} for distinct 𝑦 ∈ 𝐴 are disjoint. (Contributed by AV, 6-May-2020.) |
⊢ Disj 𝑦 ∈ 𝐴 {𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦} | ||
Theorem | disjiun 5061* | A disjoint collection yields disjoint indexed unions for disjoint index sets. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 14-Nov-2016.) |
⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ (𝐶 ∩ 𝐷) = ∅)) → (∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵) = ∅) | ||
Theorem | disjord 5062* | Conditions for a collection of sets 𝐴(𝑎) for 𝑎 ∈ 𝑉 to be disjoint. (Contributed by AV, 9-Jan-2022.) |
⊢ (𝑎 = 𝑏 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑎 = 𝑏) ⇒ ⊢ (𝜑 → Disj 𝑎 ∈ 𝑉 𝐴) | ||
Theorem | disjiunb 5063* | Two ways to say that a collection of index unions 𝐶(𝑖, 𝑥) for 𝑖 ∈ 𝐴 and 𝑥 ∈ 𝐵 is disjoint. (Contributed by AV, 9-Jan-2022.) |
⊢ (𝑖 = 𝑗 → 𝐵 = 𝐷) & ⊢ (𝑖 = 𝑗 → 𝐶 = 𝐸) ⇒ ⊢ (Disj 𝑖 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (∪ 𝑥 ∈ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ 𝐷 𝐸) = ∅)) | ||
Theorem | disjiund 5064* | Conditions for a collection of index unions of sets 𝐴(𝑎, 𝑏) for 𝑎 ∈ 𝑉 and 𝑏 ∈ 𝑊 to be disjoint. (Contributed by AV, 9-Jan-2022.) |
⊢ (𝑎 = 𝑐 → 𝐴 = 𝐶) & ⊢ (𝑏 = 𝑑 → 𝐶 = 𝐷) & ⊢ (𝑎 = 𝑐 → 𝑊 = 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐷) → 𝑎 = 𝑐) ⇒ ⊢ (𝜑 → Disj 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ 𝑊 𝐴) | ||
Theorem | sndisj 5065 | Any collection of singletons is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Disj 𝑥 ∈ 𝐴 {𝑥} | ||
Theorem | 0disj 5066 | Any collection of empty sets is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Disj 𝑥 ∈ 𝐴 ∅ | ||
Theorem | disjxsn 5067* | A singleton collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Disj 𝑥 ∈ {𝐴}𝐵 | ||
Theorem | disjx0 5068 | An empty collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Disj 𝑥 ∈ ∅ 𝐵 | ||
Theorem | disjprgw 5069* | Version of disjprg 5070 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → (Disj 𝑥 ∈ {𝐴, 𝐵}𝐶 ↔ (𝐷 ∩ 𝐸) = ∅)) | ||
Theorem | disjprg 5070* | A pair collection is disjoint iff the two sets in the family have empty intersection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → (Disj 𝑥 ∈ {𝐴, 𝐵}𝐶 ↔ (𝐷 ∩ 𝐸) = ∅)) | ||
Theorem | disjxiun 5071* | An indexed union of a disjoint collection of disjoint collections is disjoint if each component is disjoint, and the disjoint unions in the collection are also disjoint. Note that 𝐵(𝑦) and 𝐶(𝑥) may have the displayed free variables. (Contributed by Mario Carneiro, 14-Nov-2016.) (Proof shortened by JJ, 27-May-2021.) |
⊢ (Disj 𝑦 ∈ 𝐴 𝐵 → (Disj 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 ↔ (∀𝑦 ∈ 𝐴 Disj 𝑥 ∈ 𝐵 𝐶 ∧ Disj 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶))) | ||
Theorem | disjxun 5072* | The union of two disjoint collections. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ ((𝐴 ∩ 𝐵) = ∅ → (Disj 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ (Disj 𝑥 ∈ 𝐴 𝐶 ∧ Disj 𝑥 ∈ 𝐵 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝐶 ∩ 𝐷) = ∅))) | ||
Theorem | disjss3 5073* | Expand a disjoint collection with any number of empty sets. (Contributed by Mario Carneiro, 15-Nov-2016.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐴)𝐶 = ∅) → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)) | ||
Syntax | wbr 5074 | Extend wff notation to include the general binary relation predicate. Note that the syntax is simply three class symbols in a row. Since binary relations are the only possible wff expressions consisting of three class expressions in a row, the syntax is unambiguous. (For an example of how syntax could become ambiguous if we are not careful, see the comment in cneg 11194.) |
wff 𝐴𝑅𝐵 | ||
Definition | df-br 5075 | Define a general binary relation. Note that the syntax is simply three class symbols in a row. Definition 6.18 of [TakeutiZaring] p. 29 generalized to arbitrary classes. Class 𝑅 often denotes a relation such as "< " that compares two classes 𝐴 and 𝐵, which might be numbers such as 1 and 2 (see df-ltxr 11002 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {〈2, 6〉, 〈3, 9〉} → 3𝑅9) (ex-br 28781). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5592, and in particular 𝑅 may be a function (see df-fun 6429). This definition of relations is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e., are not sets). On the other hand, we often find uses for this definition when 𝑅 is a proper class (see for example iprc 7751). (Contributed by NM, 31-Dec-1993.) |
⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | ||
Theorem | breq 5076 | Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.) |
⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) | ||
Theorem | breq1 5077 | Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.) |
⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) | ||
Theorem | breq2 5078 | Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.) |
⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)) | ||
Theorem | breq12 5079 | Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | ||
Theorem | breqi 5080 | Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵) | ||
Theorem | breq1i 5081 | Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶) | ||
Theorem | breq2i 5082 | Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵) | ||
Theorem | breq12i 5083 | Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷) | ||
Theorem | breq1d 5084 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) | ||
Theorem | breqd 5085 | Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷)) | ||
Theorem | breq2d 5086 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)) | ||
Theorem | breq12d 5087 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | ||
Theorem | breq123d 5088 | Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑆𝐷)) | ||
Theorem | breqdi 5089 | Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶𝐴𝐷) ⇒ ⊢ (𝜑 → 𝐶𝐵𝐷) | ||
Theorem | breqan12d 5090 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | ||
Theorem | breqan12rd 5091 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | ||
Theorem | eqnbrtrd 5092 | Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → ¬ 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐴𝑅𝐶) | ||
Theorem | nbrne1 5093 | Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.) |
⊢ ((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑅𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | nbrne2 5094 | Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.) |
⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵) | ||
Theorem | eqbrtri 5095 | Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐵𝑅𝐶 ⇒ ⊢ 𝐴𝑅𝐶 | ||
Theorem | eqbrtrd 5096 | Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqbrtrri 5097 | Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐴𝑅𝐶 ⇒ ⊢ 𝐵𝑅𝐶 | ||
Theorem | eqbrtrrd 5098 | Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐵𝑅𝐶) | ||
Theorem | breqtri 5099 | Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴𝑅𝐶 | ||
Theorem | breqtrd 5100 | Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |