P. 51 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 5001-5100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	2iunin 5001*	Rearrange indexed unions over intersection. (Contributed by NM, 18-Dec-2008.)
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 (𝐶 ∩ 𝐷) = (∪ 𝑥 ∈ 𝐴 𝐶 ∩ ∪ 𝑦 ∈ 𝐵 𝐷)
Theorem	iindif2 5002*	Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use uniiun 4984 to recover Enderton's theorem. (Contributed by NM, 5-Oct-2006.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶))
Theorem	iinin2 5003*	Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4985 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶))
Theorem	iinin1 5004*	Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4985 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵) = (∩ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵))
Theorem	iinvdif 5005*	The indexed intersection of a complement. (Contributed by Gérard Lang, 5-Aug-2018.)
⊢ ∩ 𝑥 ∈ 𝐴 (V ∖ 𝐵) = (V ∖ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	elriin 5006*	Elementhood in a relative intersection. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝐵 ∈ (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) ↔ (𝐵 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑆))
Theorem	riin0 5007*	Relative intersection of an empty family. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 = ∅ → (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) = 𝐴)
Theorem	riinn0 5008*	Relative intersection of a nonempty family. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((∀𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅) → (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) = ∩ 𝑥 ∈ 𝑋 𝑆)
Theorem	riinrab 5009*	Relative intersection of a relative abstraction. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 {𝑦 ∈ 𝐴 ∣ 𝜑}) = {𝑦 ∈ 𝐴 ∣ ∀𝑥 ∈ 𝑋 𝜑}
Theorem	symdif0 5010	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 5011	The symmetric difference with the universal class is the complement. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 △ V) = (V ∖ 𝐴)
Theorem	symdifid 5012	The symmetric difference of a class with itself is the empty class. (Contributed by Scott Fenton, 25-Apr-2012.)
⊢ (𝐴 △ 𝐴) = ∅
Theorem	iinxsng 5013*	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 5014*	Indexed intersection with an unordered pair index. (Contributed by NM, 25-Jan-2012.)
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∩ 𝐸))
Theorem	iunxsng 5015*	A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶)
Theorem	iunxsn 5016*	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 5017*	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 5018	Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∪ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	iunxun 5019	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 5020*	An indexed union where some terms are the empty set. See iunxdif2 4979. (Contributed by Thierry Arnoux, 4-May-2020.)
⊢ Ⅎ𝑥𝐸    ⇒   ⊢ (∀𝑥 ∈ 𝐸 𝐵 = ∅ → ∪ 𝑥 ∈ (𝐴 ∖ 𝐸)𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	iunxprg 5021*	A pair index picks out two instances of an indexed union's argument. (Contributed by Alexander van der Vekens, 2-Feb-2018.)
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∪ 𝐸))
Theorem	iunxiun 5022*	Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016.)
⊢ ∪ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 = ∪ 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶
Theorem	iinuni 5023*	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 5024*	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 5025	Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)
Theorem	pwssb 5026*	Two ways to express a collection of subclasses. (Contributed by NM, 19-Jul-2006.)
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
Theorem	elpwpw 5027	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 5028*	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 5029*	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 5030	Relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
⊢ (𝐵 ∈ 𝐴 → (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 = 𝐵))
Theorem	iinpw 5031*	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 5032*	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 5033	A nonempty intersection of a family of subsets of a class is included in that class. (Contributed by BJ, 7-Dec-2021.)
⊢ (𝐴 ⊆ 𝒫 𝑋 → (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ 𝑋))
Theorem	rintn0 5034	Relative intersection of a nonempty set. (Contributed by Stefan O'Rear, 3-Apr-2015.) (Revised by Mario Carneiro, 5-Jun-2015.)
⊢ ((𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅) → (𝐴 ∩ ∩ 𝑋) = ∩ 𝑋)
2.1.22  Disjointness
Syntax	wdisj 5035	Extend wff notation to include the statement that a family of classes 𝐵(𝑥), for 𝑥 ∈ 𝐴, is a disjoint family.
wff Disj 𝑥 ∈ 𝐴 𝐵
Definition	df-disj 5036*	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 5037*	Alternate definition for disjoint classes. (Contributed by NM, 17-Jun-2017.)
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
Theorem	disjss2 5038	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 5039	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑥 ∈ 𝐴 𝐶))
Theorem	disjeq2dv 5040*	Equality deduction for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑥 ∈ 𝐴 𝐶))
Theorem	disjss1 5041*	A subset of a disjoint collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶))
Theorem	disjeq1 5042*	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝐴 = 𝐵 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶))
Theorem	disjeq1d 5043*	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶))
Theorem	disjeq12d 5044*	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷))
Theorem	cbvdisj 5045*	Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶)
Theorem	cbvdisjv 5046*	Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 11-Dec-2016.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶)
Theorem	nfdisjw 5047*	Bound-variable hypothesis builder for disjoint collection. Version of nfdisj 5048 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 5048	Bound-variable hypothesis builder for disjoint collection. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker nfdisjw 5047 when possible. (Contributed by Mario Carneiro, 14-Nov-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦Disj 𝑥 ∈ 𝐴 𝐵
Theorem	nfdisj1 5049	Bound-variable hypothesis builder for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Ⅎ𝑥Disj 𝑥 ∈ 𝐴 𝐵
Theorem	disjor 5050*	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 5051*	Two ways to say that a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
Theorem	disji2 5052*	Property of a disjoint collection: if 𝐵(𝑋) = 𝐶 and 𝐵(𝑌) = 𝐷, and 𝑋 ≠ 𝑌, then 𝐶 and 𝐷 are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷)    ⇒   ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝑋 ≠ 𝑌) → (𝐶 ∩ 𝐷) = ∅)
Theorem	disji 5053*	Property of a disjoint collection: if 𝐵(𝑋) = 𝐶 and 𝐵(𝑌) = 𝐷 have a common element 𝑍, then 𝑋 = 𝑌. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷)    ⇒   ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (𝑍 ∈ 𝐶 ∧ 𝑍 ∈ 𝐷)) → 𝑋 = 𝑌)
Theorem	invdisj 5054*	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 5055*	Version of invdisjrab 5056 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Gino Giotto, 26-Jan-2024.)
⊢ Disj 𝑦 ∈ 𝐴 {𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦}
Theorem	invdisjrab 5056*	The restricted class abstractions {𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦} for distinct 𝑦 ∈ 𝐴 are disjoint. (Contributed by AV, 6-May-2020.)
⊢ Disj 𝑦 ∈ 𝐴 {𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦}
Theorem	disjiun 5057*	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 5058*	Conditions for a collection of sets 𝐴(𝑎) for 𝑎 ∈ 𝑉 to be disjoint. (Contributed by AV, 9-Jan-2022.)
⊢ (𝑎 = 𝑏 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑎 = 𝑏)    ⇒   ⊢ (𝜑 → Disj 𝑎 ∈ 𝑉 𝐴)
Theorem	disjiunb 5059*	Two ways to say that a collection of index unions 𝐶(𝑖, 𝑥) for 𝑖 ∈ 𝐴 and 𝑥 ∈ 𝐵 is disjoint. (Contributed by AV, 9-Jan-2022.)
⊢ (𝑖 = 𝑗 → 𝐵 = 𝐷)    &   ⊢ (𝑖 = 𝑗 → 𝐶 = 𝐸)    ⇒   ⊢ (Disj 𝑖 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (∪ 𝑥 ∈ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ 𝐷 𝐸) = ∅))
Theorem	disjiund 5060*	Conditions for a collection of index unions of sets 𝐴(𝑎, 𝑏) for 𝑎 ∈ 𝑉 and 𝑏 ∈ 𝑊 to be disjoint. (Contributed by AV, 9-Jan-2022.)
⊢ (𝑎 = 𝑐 → 𝐴 = 𝐶)    &   ⊢ (𝑏 = 𝑑 → 𝐶 = 𝐷)    &   ⊢ (𝑎 = 𝑐 → 𝑊 = 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐷) → 𝑎 = 𝑐)    ⇒   ⊢ (𝜑 → Disj 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ 𝑊 𝐴)
Theorem	sndisj 5061	Any collection of singletons is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ 𝐴 {𝑥}
Theorem	0disj 5062	Any collection of empty sets is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ 𝐴 ∅
Theorem	disjxsn 5063*	A singleton collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ {𝐴}𝐵
Theorem	disjx0 5064	An empty collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ ∅ 𝐵
Theorem	disjprgw 5065*	Version of disjprg 5066 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Gino Giotto, 26-Jan-2024.)
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → (Disj 𝑥 ∈ {𝐴, 𝐵}𝐶 ↔ (𝐷 ∩ 𝐸) = ∅))
Theorem	disjprg 5066*	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 5067*	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 5068*	The union of two disjoint collections. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝐴 ∩ 𝐵) = ∅ → (Disj 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ (Disj 𝑥 ∈ 𝐴 𝐶 ∧ Disj 𝑥 ∈ 𝐵 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝐶 ∩ 𝐷) = ∅)))
Theorem	disjss3 5069*	Expand a disjoint collection with any number of empty sets. (Contributed by Mario Carneiro, 15-Nov-2016.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐴)𝐶 = ∅) → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶))
2.1.23  Binary relations
Syntax	wbr 5070	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 11136.)
wff 𝐴𝑅𝐵
Definition	df-br 5071	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 10945 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 28696). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5587, and in particular 𝑅 may be a function (see df-fun 6420). 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 7734). (Contributed by NM, 31-Dec-1993.)
⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Theorem	breq 5072	Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.)
⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵))
Theorem	breq1 5073	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
Theorem	breq2 5074	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))
Theorem	breq12 5075	Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
Theorem	breqi 5076	Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)
Theorem	breq1i 5077	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)
Theorem	breq2i 5078	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)
Theorem	breq12i 5079	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)
Theorem	breq1d 5080	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
Theorem	breqd 5081	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))
Theorem	breq2d 5082	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))
Theorem	breq12d 5083	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
Theorem	breq123d 5084	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑅 = 𝑆)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑆𝐷))
Theorem	breqdi 5085	Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 5-Oct-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶𝐴𝐷)    ⇒   ⊢ (𝜑 → 𝐶𝐵𝐷)
Theorem	breqan12d 5086	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
Theorem	breqan12rd 5087	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
Theorem	eqnbrtrd 5088	Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → ¬ 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → ¬ 𝐴𝑅𝐶)
Theorem	nbrne1 5089	Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
⊢ ((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑅𝐶) → 𝐵 ≠ 𝐶)
Theorem	nbrne2 5090	Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
⊢ ((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴 ≠ 𝐵)
Theorem	eqbrtri 5091	Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵𝑅𝐶    ⇒   ⊢ 𝐴𝑅𝐶
Theorem	eqbrtrd 5092	Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqbrtrri 5093	Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴𝑅𝐶    ⇒   ⊢ 𝐵𝑅𝐶
Theorem	eqbrtrrd 5094	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐵𝑅𝐶)
Theorem	breqtri 5095	Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴𝑅𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴𝑅𝐶
Theorem	breqtrd 5096	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	breqtrri 5097	Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴𝑅𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴𝑅𝐶
Theorem	breqtrrd 5098	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	3brtr3i 5099	Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴𝑅𝐵    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ 𝐶𝑅𝐷
Theorem	3brtr4i 5100	Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴𝑅𝐵    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ 𝐶𝑅𝐷