![]() |
Metamath
Proof Explorer Theorem List (p. 52 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iunxiun 5101* | Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016.) |
⊢ ∪ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 = ∪ 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 | ||
Theorem | iinuni 5102* | 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 5103* | 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 5104 | Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.) |
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵) | ||
Theorem | pwssb 5105* | Two ways to express a collection of subclasses. (Contributed by NM, 19-Jul-2006.) |
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) | ||
Theorem | elpwpw 5106 | 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 5107* | 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 5108* | 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 5109 | Relationship for power class and union. (Contributed by NM, 18-Jul-2006.) |
⊢ (𝐵 ∈ 𝐴 → (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 = 𝐵)) | ||
Theorem | iinpw 5110* | 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 5111* | 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 5112 | A nonempty intersection of a family of subsets of a class is included in that class. (Contributed by BJ, 7-Dec-2021.) |
⊢ (𝐴 ⊆ 𝒫 𝑋 → (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ 𝑋)) | ||
Theorem | rintn0 5113 | Relative intersection of a nonempty set. (Contributed by Stefan O'Rear, 3-Apr-2015.) (Revised by Mario Carneiro, 5-Jun-2015.) |
⊢ ((𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅) → (𝐴 ∩ ∩ 𝑋) = ∩ 𝑋) | ||
Syntax | wdisj 5114 | Extend wff notation to include the statement that a family of classes 𝐵(𝑥), for 𝑥 ∈ 𝐴, is a disjoint family. |
wff Disj 𝑥 ∈ 𝐴 𝐵 | ||
Definition | df-disj 5115* | 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 5116* | Alternate definition for disjoint classes. (Contributed by NM, 17-Jun-2017.) |
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | ||
Theorem | disjss2 5117 | 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 5118 | Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑥 ∈ 𝐴 𝐶)) | ||
Theorem | disjeq2dv 5119* | Equality deduction for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑥 ∈ 𝐴 𝐶)) | ||
Theorem | disjss1 5120* | A subset of a disjoint collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶)) | ||
Theorem | disjeq1 5121* | Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝐴 = 𝐵 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)) | ||
Theorem | disjeq1d 5122* | Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)) | ||
Theorem | disjeq12d 5123* | Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷)) | ||
Theorem | cbvdisj 5124* | Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶) | ||
Theorem | cbvdisjv 5125* | Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 11-Dec-2016.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶) | ||
Theorem | nfdisjw 5126* | Bound-variable hypothesis builder for disjoint collection. Version of nfdisj 5127 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Mario Carneiro, 14-Nov-2016.) Avoid ax-13 2372. (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦Disj 𝑥 ∈ 𝐴 𝐵 | ||
Theorem | nfdisj 5127 | Bound-variable hypothesis builder for disjoint collection. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker nfdisjw 5126 when possible. (Contributed by Mario Carneiro, 14-Nov-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦Disj 𝑥 ∈ 𝐴 𝐵 | ||
Theorem | nfdisj1 5128 | Bound-variable hypothesis builder for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Ⅎ𝑥Disj 𝑥 ∈ 𝐴 𝐵 | ||
Theorem | disjor 5129* | 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 5130* | Two ways to say that a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) | ||
Theorem | disji2 5131* | Property of a disjoint collection: if 𝐵(𝑋) = 𝐶 and 𝐵(𝑌) = 𝐷, and 𝑋 ≠ 𝑌, then 𝐶 and 𝐷 are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) ⇒ ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝑋 ≠ 𝑌) → (𝐶 ∩ 𝐷) = ∅) | ||
Theorem | disji 5132* | Property of a disjoint collection: if 𝐵(𝑋) = 𝐶 and 𝐵(𝑌) = 𝐷 have a common element 𝑍, then 𝑋 = 𝑌. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) ⇒ ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (𝑍 ∈ 𝐶 ∧ 𝑍 ∈ 𝐷)) → 𝑋 = 𝑌) | ||
Theorem | invdisj 5133* | 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 5134* | Version of invdisjrab 5135 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ Disj 𝑦 ∈ 𝐴 {𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦} | ||
Theorem | invdisjrab 5135* | The restricted class abstractions {𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦} for distinct 𝑦 ∈ 𝐴 are disjoint. (Contributed by AV, 6-May-2020.) |
⊢ Disj 𝑦 ∈ 𝐴 {𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦} | ||
Theorem | disjiun 5136* | 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 5137* | Conditions for a collection of sets 𝐴(𝑎) for 𝑎 ∈ 𝑉 to be disjoint. (Contributed by AV, 9-Jan-2022.) |
⊢ (𝑎 = 𝑏 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑎 = 𝑏) ⇒ ⊢ (𝜑 → Disj 𝑎 ∈ 𝑉 𝐴) | ||
Theorem | disjiunb 5138* | Two ways to say that a collection of index unions 𝐶(𝑖, 𝑥) for 𝑖 ∈ 𝐴 and 𝑥 ∈ 𝐵 is disjoint. (Contributed by AV, 9-Jan-2022.) |
⊢ (𝑖 = 𝑗 → 𝐵 = 𝐷) & ⊢ (𝑖 = 𝑗 → 𝐶 = 𝐸) ⇒ ⊢ (Disj 𝑖 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (∪ 𝑥 ∈ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ 𝐷 𝐸) = ∅)) | ||
Theorem | disjiund 5139* | Conditions for a collection of index unions of sets 𝐴(𝑎, 𝑏) for 𝑎 ∈ 𝑉 and 𝑏 ∈ 𝑊 to be disjoint. (Contributed by AV, 9-Jan-2022.) |
⊢ (𝑎 = 𝑐 → 𝐴 = 𝐶) & ⊢ (𝑏 = 𝑑 → 𝐶 = 𝐷) & ⊢ (𝑎 = 𝑐 → 𝑊 = 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐷) → 𝑎 = 𝑐) ⇒ ⊢ (𝜑 → Disj 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ 𝑊 𝐴) | ||
Theorem | sndisj 5140 | Any collection of singletons is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Disj 𝑥 ∈ 𝐴 {𝑥} | ||
Theorem | 0disj 5141 | Any collection of empty sets is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Disj 𝑥 ∈ 𝐴 ∅ | ||
Theorem | disjxsn 5142* | A singleton collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Disj 𝑥 ∈ {𝐴}𝐵 | ||
Theorem | disjx0 5143 | An empty collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Disj 𝑥 ∈ ∅ 𝐵 | ||
Theorem | disjprgw 5144* | Version of disjprg 5145 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → (Disj 𝑥 ∈ {𝐴, 𝐵}𝐶 ↔ (𝐷 ∩ 𝐸) = ∅)) | ||
Theorem | disjprg 5145* | 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 5146* | 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 5147* | The union of two disjoint collections. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ ((𝐴 ∩ 𝐵) = ∅ → (Disj 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ (Disj 𝑥 ∈ 𝐴 𝐶 ∧ Disj 𝑥 ∈ 𝐵 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝐶 ∩ 𝐷) = ∅))) | ||
Theorem | disjss3 5148* | Expand a disjoint collection with any number of empty sets. (Contributed by Mario Carneiro, 15-Nov-2016.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐴)𝐶 = ∅) → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)) | ||
Syntax | wbr 5149 | 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 11445.) |
wff 𝐴𝑅𝐵 | ||
Definition | df-br 5150 | 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 11253 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 29684). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5684, and in particular 𝑅 may be a function (see df-fun 6546). 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 7904). (Contributed by NM, 31-Dec-1993.) |
⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅) | ||
Theorem | breq 5151 | Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.) |
⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)) | ||
Theorem | breq1 5152 | Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.) |
⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) | ||
Theorem | breq2 5153 | Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.) |
⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)) | ||
Theorem | breq12 5154 | Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | ||
Theorem | breqi 5155 | Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵) | ||
Theorem | breq1i 5156 | Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶) | ||
Theorem | breq2i 5157 | Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵) | ||
Theorem | breq12i 5158 | Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷) | ||
Theorem | breq1d 5159 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) | ||
Theorem | breqd 5160 | Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷)) | ||
Theorem | breq2d 5161 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)) | ||
Theorem | breq12d 5162 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | ||
Theorem | breq123d 5163 | Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑆𝐷)) | ||
Theorem | breqdi 5164 | Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 5-Oct-2020.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶𝐴𝐷) ⇒ ⊢ (𝜑 → 𝐶𝐵𝐷) | ||
Theorem | breqan12d 5165 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | ||
Theorem | breqan12rd 5166 | Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | ||
Theorem | eqnbrtrd 5167 | Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → ¬ 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐴𝑅𝐶) | ||
Theorem | nbrne1 5168 | Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.) |
⊢ ((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑅𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | nbrne2 5169 | Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.) |
⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵) | ||
Theorem | eqbrtri 5170 | Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐵𝑅𝐶 ⇒ ⊢ 𝐴𝑅𝐶 | ||
Theorem | eqbrtrd 5171 | Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqbrtrri 5172 | Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐴𝑅𝐶 ⇒ ⊢ 𝐵𝑅𝐶 | ||
Theorem | eqbrtrrd 5173 | Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐵𝑅𝐶) | ||
Theorem | breqtri 5174 | Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴𝑅𝐶 | ||
Theorem | breqtrd 5175 | Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrri 5176 | Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴𝑅𝐶 | ||
Theorem | breqtrrd 5177 | Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | 3brtr3i 5178 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ 𝐶𝑅𝐷 | ||
Theorem | 3brtr4i 5179 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ 𝐶𝑅𝐷 | ||
Theorem | 3brtr3d 5180 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) | ||
Theorem | 3brtr4d 5181 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐶 = 𝐴) & ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) | ||
Theorem | 3brtr3g 5182 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) | ||
Theorem | 3brtr4g 5183 | Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶𝑅𝐷) | ||
Theorem | eqbrtrid 5184 | A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqbrtrrid 5185 | A chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.) |
⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrid 5186 | A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
⊢ 𝐴𝑅𝐵 & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrrid 5187 | A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) |
⊢ 𝐴𝑅𝐵 & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqbrtrdi 5188 | A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐵𝑅𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqbrtrrdi 5189 | A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.) |
⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ 𝐵𝑅𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrdi 5190 | A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | breqtrrdi 5191 | A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) |
⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | ssbrd 5192 | Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷)) | ||
Theorem | ssbr 5193 | Implication from a subclass relationship of binary relations. (Contributed by Peter Mazsa, 11-Nov-2019.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷)) | ||
Theorem | ssbri 5194 | Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ (𝐶𝐴𝐷 → 𝐶𝐵𝐷) | ||
Theorem | nfbrd 5195 | Deduction version of bound-variable hypothesis builder nfbr 5196. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝑅) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴𝑅𝐵) | ||
Theorem | nfbr 5196 | Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴𝑅𝐵 | ||
Theorem | brab1 5197* | Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.) |
⊢ (𝑥𝑅𝐴 ↔ 𝑥 ∈ {𝑧 ∣ 𝑧𝑅𝐴}) | ||
Theorem | br0 5198 | The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.) |
⊢ ¬ 𝐴∅𝐵 | ||
Theorem | brne0 5199 | If two sets are in a binary relation, the relation cannot be empty. (Contributed by Alexander van der Vekens, 7-Jul-2018.) |
⊢ (𝐴𝑅𝐵 → 𝑅 ≠ ∅) | ||
Theorem | brun 5200 | The union of two binary relations. (Contributed by NM, 21-Dec-2008.) |
⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |