Home | Metamath
Proof Explorer Theorem List (p. 51 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | symdifid 5001 | The symmetric difference of a class with itself is the empty class. (Contributed by Scott Fenton, 25-Apr-2012.) |
⊢ (𝐴 △ 𝐴) = ∅ | ||
Theorem | iinxsng 5002* | 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 5003* | Indexed intersection with an unordered pair index. (Contributed by NM, 25-Jan-2012.) |
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∩ 𝐸)) | ||
Theorem | iunxsng 5004* | A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶) | ||
Theorem | iunxsn 5005* | 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 5006* | 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 2383. (Revised by Gino Giotto, 19-May-2023.) |
⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶) | ||
Theorem | iunun 5007 | Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∪ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ ∪ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | iunxun 5008 | 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 5009* | An indexed union where some terms are the empty set. See iunxdif2 4969. (Contributed by Thierry Arnoux, 4-May-2020.) |
⊢ Ⅎ𝑥𝐸 ⇒ ⊢ (∀𝑥 ∈ 𝐸 𝐵 = ∅ → ∪ 𝑥 ∈ (𝐴 ∖ 𝐸)𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | iunxprg 5010* | A pair index picks out two instances of an indexed union's argument. (Contributed by Alexander van der Vekens, 2-Feb-2018.) |
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∪ 𝐸)) | ||
Theorem | iunxiun 5011* | Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016.) |
⊢ ∪ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 = ∪ 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 | ||
Theorem | iinuni 5012* | 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 5013* | 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 5014 | Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.) |
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵) | ||
Theorem | pwssb 5015* | Two ways to express a collection of subclasses. (Contributed by NM, 19-Jul-2006.) |
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) | ||
Theorem | elpwpw 5016 | 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 5017* | 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 5018* | 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 5019 | Relationship for power class and union. (Contributed by NM, 18-Jul-2006.) |
⊢ (𝐵 ∈ 𝐴 → (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 = 𝐵)) | ||
Theorem | iinpw 5020* | 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 5021* | 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 | rintn0 5022 | Relative intersection of a nonempty set. (Contributed by Stefan O'Rear, 3-Apr-2015.) (Revised by Mario Carneiro, 5-Jun-2015.) |
⊢ ((𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅) → (𝐴 ∩ ∩ 𝑋) = ∩ 𝑋) | ||
Syntax | wdisj 5023 | Extend wff notation to include the statement that a family of classes 𝐵(𝑥), for 𝑥 ∈ 𝐴, is a disjoint family. |
wff Disj 𝑥 ∈ 𝐴 𝐵 | ||
Definition | df-disj 5024* | 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 5025* | Alternate definition for disjoint classes. (Contributed by NM, 17-Jun-2017.) |
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | ||
Theorem | disjss2 5026 | 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 5027 | Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑥 ∈ 𝐴 𝐶)) | ||
Theorem | disjeq2dv 5028* | Equality deduction for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑥 ∈ 𝐴 𝐶)) | ||
Theorem | disjss1 5029* | A subset of a disjoint collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶)) | ||
Theorem | disjeq1 5030* | Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝐴 = 𝐵 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)) | ||
Theorem | disjeq1d 5031* | Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)) | ||
Theorem | disjeq12d 5032* | Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷)) | ||
Theorem | cbvdisj 5033* | Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶) | ||
Theorem | cbvdisjv 5034* | Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 11-Dec-2016.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶) | ||
Theorem | nfdisjw 5035* | Version of nfdisj 5036 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦Disj 𝑥 ∈ 𝐴 𝐵 | ||
Theorem | nfdisj 5036 | Bound-variable hypothesis builder for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦Disj 𝑥 ∈ 𝐴 𝐵 | ||
Theorem | nfdisj1 5037 | Bound-variable hypothesis builder for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Ⅎ𝑥Disj 𝑥 ∈ 𝐴 𝐵 | ||
Theorem | disjor 5038* | 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 5039* | Two ways to say that a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) | ||
Theorem | disji2 5040* | Property of a disjoint collection: if 𝐵(𝑋) = 𝐶 and 𝐵(𝑌) = 𝐷, and 𝑋 ≠ 𝑌, then 𝐶 and 𝐷 are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) ⇒ ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝑋 ≠ 𝑌) → (𝐶 ∩ 𝐷) = ∅) | ||
Theorem | disji 5041* | Property of a disjoint collection: if 𝐵(𝑋) = 𝐶 and 𝐵(𝑌) = 𝐷 have a common element 𝑍, then 𝑋 = 𝑌. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) ⇒ ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (𝑍 ∈ 𝐶 ∧ 𝑍 ∈ 𝐷)) → 𝑋 = 𝑌) | ||
Theorem | invdisj 5042* | 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 5043* | Version of invdisjrab 5044 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ Disj 𝑦 ∈ 𝐴 {𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦} | ||
Theorem | invdisjrab 5044* | The restricted class abstractions {𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦} for distinct 𝑦 ∈ 𝐴 are disjoint. (Contributed by AV, 6-May-2020.) |
⊢ Disj 𝑦 ∈ 𝐴 {𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦} | ||
Theorem | disjiun 5045* | 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 5046* | Conditions for a collection of sets 𝐴(𝑎) for 𝑎 ∈ 𝑉 to be disjoint. (Contributed by AV, 9-Jan-2022.) |
⊢ (𝑎 = 𝑏 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑎 = 𝑏) ⇒ ⊢ (𝜑 → Disj 𝑎 ∈ 𝑉 𝐴) | ||
Theorem | disjiunb 5047* | Two ways to say that a collection of index unions 𝐶(𝑖, 𝑥) for 𝑖 ∈ 𝐴 and 𝑥 ∈ 𝐵 is disjoint. (Contributed by AV, 9-Jan-2022.) |
⊢ (𝑖 = 𝑗 → 𝐵 = 𝐷) & ⊢ (𝑖 = 𝑗 → 𝐶 = 𝐸) ⇒ ⊢ (Disj 𝑖 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (∪ 𝑥 ∈ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ 𝐷 𝐸) = ∅)) | ||
Theorem | disjiund 5048* | Conditions for a collection of index unions of sets 𝐴(𝑎, 𝑏) for 𝑎 ∈ 𝑉 and 𝑏 ∈ 𝑊 to be disjoint. (Contributed by AV, 9-Jan-2022.) |
⊢ (𝑎 = 𝑐 → 𝐴 = 𝐶) & ⊢ (𝑏 = 𝑑 → 𝐶 = 𝐷) & ⊢ (𝑎 = 𝑐 → 𝑊 = 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐷) → 𝑎 = 𝑐) ⇒ ⊢ (𝜑 → Disj 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ 𝑊 𝐴) | ||
Theorem | sndisj 5049 | Any collection of singletons is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Disj 𝑥 ∈ 𝐴 {𝑥} | ||
Theorem | 0disj 5050 | Any collection of empty sets is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Disj 𝑥 ∈ 𝐴 ∅ | ||
Theorem | disjxsn 5051* | A singleton collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Disj 𝑥 ∈ {𝐴}𝐵 | ||
Theorem | disjx0 5052 | An empty collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Disj 𝑥 ∈ ∅ 𝐵 | ||
Theorem | disjprgw 5053* | Version of disjprg 5054 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → (Disj 𝑥 ∈ {𝐴, 𝐵}𝐶 ↔ (𝐷 ∩ 𝐸) = ∅)) | ||
Theorem | disjprg 5054* | 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 5055* | 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 5056* | The union of two disjoint collections. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ ((𝐴 ∩ 𝐵) = ∅ → (Disj 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ (Disj 𝑥 ∈ 𝐴 𝐶 ∧ Disj 𝑥 ∈ 𝐵 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝐶 ∩ 𝐷) = ∅))) | ||
Theorem | disjss3 5057* | Expand a disjoint collection with any number of empty sets. (Contributed by Mario Carneiro, 15-Nov-2016.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐴)𝐶 = ∅) → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)) | ||
Syntax | wbr 5058 | 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 10860.) |
wff 𝐴𝑅𝐵 | ||
Definition | df-br 5059 | 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 10669 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {〈2, 6〉, 〈3, 9〉} → 3𝑅9) (ex-br 28138). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5556, and in particular 𝑅 may be a function (see df-fun 6351). 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 7606). (Contributed by NM, 31-Dec-1993.) |
⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | ||
Theorem | breq 5060 | Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.) |
⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) | ||
Theorem | breq1 5061 | Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.) |
⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) | ||
Theorem | breq2 5062 | Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.) |
⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)) | ||
Theorem | breq12 5063 | Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | ||
Theorem | breqi 5064 | Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵) | ||
Theorem | breq1i 5065 | Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶) | ||
Theorem | breq2i 5066 | Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵) | ||
Theorem | breq12i 5067 | Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷) | ||
Theorem | breq1d 5068 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) | ||
Theorem | breqd 5069 | Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷)) | ||
Theorem | breq2d 5070 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)) | ||
Theorem | breq12d 5071 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | ||
Theorem | breq123d 5072 | Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑆𝐷)) | ||
Theorem | breqdi 5073 | Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶𝐴𝐷) ⇒ ⊢ (𝜑 → 𝐶𝐵𝐷) | ||
Theorem | breqan12d 5074 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | ||
Theorem | breqan12rd 5075 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | ||
Theorem | eqnbrtrd 5076 | Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → ¬ 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐴𝑅𝐶) | ||
Theorem | nbrne1 5077 | Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.) |
⊢ ((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑅𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | nbrne2 5078 | Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.) |
⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵) | ||
Theorem | eqbrtri 5079 | Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐵𝑅𝐶 ⇒ ⊢ 𝐴𝑅𝐶 | ||
Theorem | eqbrtrd 5080 | Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqbrtrri 5081 | Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐴𝑅𝐶 ⇒ ⊢ 𝐵𝑅𝐶 | ||
Theorem | eqbrtrrd 5082 | Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐵𝑅𝐶) | ||
Theorem | breqtri 5083 | Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴𝑅𝐶 | ||
Theorem | breqtrd 5084 | Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrri 5085 | Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴𝑅𝐶 | ||
Theorem | breqtrrd 5086 | Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | 3brtr3i 5087 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ 𝐶𝑅𝐷 | ||
Theorem | 3brtr4i 5088 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ 𝐶𝑅𝐷 | ||
Theorem | 3brtr3d 5089 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) | ||
Theorem | 3brtr4d 5090 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐶 = 𝐴) & ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) | ||
Theorem | 3brtr3g 5091 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) | ||
Theorem | 3brtr4g 5092 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) | ||
Theorem | eqbrtrid 5093 | A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqbrtrrid 5094 | A chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.) |
⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrid 5095 | A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrrid 5096 | A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) |
⊢ 𝐴𝑅𝐵 & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqbrtrdi 5097 | A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐵𝑅𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqbrtrrdi 5098 | A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.) |
⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ 𝐵𝑅𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrdi 5099 | A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrrdi 5100 | A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |