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	iinrab2 5001*	Indexed intersection of a restricted class abstraction. (Contributed by NM, 6-Dec-2011.)
⊢ (∩ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} ∩ 𝐵) = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑}
Theorem	iunin2 5002*	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4990 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.)
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	iunin1 5003*	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4990 to recover Enderton's theorem. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ ∪ 𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵) = (∪ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵)
Theorem	iinun2 5004*	Indexed intersection of union. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4991 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.)
⊢ ∩ 𝑥 ∈ 𝐴 (𝐵 ∪ 𝐶) = (𝐵 ∪ ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	iundif2 5005*	Indexed union of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use intiin 4991 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.)
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (𝐵 ∖ ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	iindif1 5006*	Indexed intersection of class difference with the subtrahend held constant. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (∩ 𝑥 ∈ 𝐴 𝐵 ∖ 𝐶))
Theorem	2iunin 5007*	Rearrange indexed unions over intersection. (Contributed by NM, 18-Dec-2008.)
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 (𝐶 ∩ 𝐷) = (∪ 𝑥 ∈ 𝐴 𝐶 ∩ ∪ 𝑦 ∈ 𝐵 𝐷)
Theorem	iindif2 5008*	Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use uniiun 4990 to recover Enderton's theorem. (Contributed by NM, 5-Oct-2006.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶))
Theorem	iinin2 5009*	Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4991 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶))
Theorem	iinin1 5010*	Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4991 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵) = (∩ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵))
Theorem	iinvdif 5011*	The indexed intersection of a complement. (Contributed by Gérard Lang, 5-Aug-2018.)
⊢ ∩ 𝑥 ∈ 𝐴 (V ∖ 𝐵) = (V ∖ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	elriin 5012*	Elementhood in a relative intersection. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝐵 ∈ (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) ↔ (𝐵 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑆))
Theorem	riin0 5013*	Relative intersection of an empty family. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 = ∅ → (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) = 𝐴)
Theorem	riinn0 5014*	Relative intersection of a nonempty family. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((∀𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅) → (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) = ∩ 𝑥 ∈ 𝑋 𝑆)
Theorem	riinrab 5015*	Relative intersection of a relative abstraction. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 {𝑦 ∈ 𝐴 ∣ 𝜑}) = {𝑦 ∈ 𝐴 ∣ ∀𝑥 ∈ 𝑋 𝜑}
Theorem	symdif0 5016	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 5017	The symmetric difference with the universal class is the complement. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 △ V) = (V ∖ 𝐴)
Theorem	symdifid 5018	The symmetric difference of a class with itself is the empty class. (Contributed by Scott Fenton, 25-Apr-2012.)
⊢ (𝐴 △ 𝐴) = ∅
Theorem	iinxsng 5019*	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 5020*	Indexed intersection with an unordered pair index. (Contributed by NM, 25-Jan-2012.)
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∩ 𝐸))
Theorem	iunxsng 5021*	A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶)
Theorem	iunxsn 5022*	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 5023*	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 2375. (Revised by GG, 19-May-2023.)
⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶)
Theorem	iunun 5024	Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∪ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	iunxun 5025	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 5026*	An indexed union where some terms are the empty set. See iunxdif2 4985. (Contributed by Thierry Arnoux, 4-May-2020.)
⊢ Ⅎ𝑥𝐸    ⇒   ⊢ (∀𝑥 ∈ 𝐸 𝐵 = ∅ → ∪ 𝑥 ∈ (𝐴 ∖ 𝐸)𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	iunxprg 5027*	A pair index picks out two instances of an indexed union's argument. (Contributed by Alexander van der Vekens, 2-Feb-2018.)
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∪ 𝐸))
Theorem	iunxiun 5028*	Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016.)
⊢ ∪ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 = ∪ 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶
Theorem	iinuni 5029*	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 5030*	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 5031	Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)
Theorem	pwssb 5032*	Two ways to express a collection of subclasses. (Contributed by NM, 19-Jul-2006.)
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
Theorem	elpwpw 5033	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 5034*	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 5035*	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 5036	Relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
⊢ (𝐵 ∈ 𝐴 → (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 = 𝐵))
Theorem	iinpw 5037*	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 5038*	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 5039	A nonempty intersection of a family of subsets of a class is included in that class. (Contributed by BJ, 7-Dec-2021.)
⊢ (𝐴 ⊆ 𝒫 𝑋 → (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ 𝑋))
Theorem	rintn0 5040	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 5041	Extend wff notation to include the statement that a family of classes 𝐵(𝑥), for 𝑥 ∈ 𝐴, is a disjoint family.
wff Disj 𝑥 ∈ 𝐴 𝐵
Definition	df-disj 5042*	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 5043*	Alternate definition for disjoint classes. (Contributed by NM, 17-Jun-2017.)
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
Theorem	disjss2 5044	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 5045	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑥 ∈ 𝐴 𝐶))
Theorem	disjeq2dv 5046*	Equality deduction for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑥 ∈ 𝐴 𝐶))
Theorem	disjss1 5047*	A subset of a disjoint collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶))
Theorem	disjeq1 5048*	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝐴 = 𝐵 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶))
Theorem	disjeq1d 5049*	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶))
Theorem	disjeq12d 5050*	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷))
Theorem	cbvdisj 5051*	Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶)
Theorem	cbvdisjv 5052*	Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 11-Dec-2016.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶)
Theorem	nfdisjw 5053*	Bound-variable hypothesis builder for disjoint collection. Version of nfdisj 5054 with a disjoint variable condition, which does not require ax-13 2375. (Contributed by Mario Carneiro, 14-Nov-2016.) Avoid ax-13 2375. (Revised by GG, 26-Jan-2024.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦Disj 𝑥 ∈ 𝐴 𝐵
Theorem	nfdisj 5054	Bound-variable hypothesis builder for disjoint collection. Usage of this theorem is discouraged because it depends on ax-13 2375. Use the weaker nfdisjw 5053 when possible. (Contributed by Mario Carneiro, 14-Nov-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦Disj 𝑥 ∈ 𝐴 𝐵
Theorem	nfdisj1 5055	Bound-variable hypothesis builder for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Ⅎ𝑥Disj 𝑥 ∈ 𝐴 𝐵
Theorem	disjor 5056*	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 5057*	Two ways to say that a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
Theorem	disji2 5058*	Property of a disjoint collection: if 𝐵(𝑋) = 𝐶 and 𝐵(𝑌) = 𝐷, and 𝑋 ≠ 𝑌, then 𝐶 and 𝐷 are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷)    ⇒   ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝑋 ≠ 𝑌) → (𝐶 ∩ 𝐷) = ∅)
Theorem	disji 5059*	Property of a disjoint collection: if 𝐵(𝑋) = 𝐶 and 𝐵(𝑌) = 𝐷 have a common element 𝑍, then 𝑋 = 𝑌. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷)    ⇒   ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (𝑍 ∈ 𝐶 ∧ 𝑍 ∈ 𝐷)) → 𝑋 = 𝑌)
Theorem	invdisj 5060*	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	invdisjrab 5061*	The restricted class abstractions {𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦} for distinct 𝑦 ∈ 𝐴 are disjoint. (Contributed by AV, 6-May-2020.) (Proof shortened by GG, 26-Jan-2024.)
⊢ Disj 𝑦 ∈ 𝐴 {𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦}
Theorem	disjiun 5062*	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 5063*	Conditions for a collection of sets 𝐴(𝑎) for 𝑎 ∈ 𝑉 to be disjoint. (Contributed by AV, 9-Jan-2022.)
⊢ (𝑎 = 𝑏 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑎 = 𝑏)    ⇒   ⊢ (𝜑 → Disj 𝑎 ∈ 𝑉 𝐴)
Theorem	disjiunb 5064*	Two ways to say that a collection of index unions 𝐶(𝑖, 𝑥) for 𝑖 ∈ 𝐴 and 𝑥 ∈ 𝐵 is disjoint. (Contributed by AV, 9-Jan-2022.)
⊢ (𝑖 = 𝑗 → 𝐵 = 𝐷)    &   ⊢ (𝑖 = 𝑗 → 𝐶 = 𝐸)    ⇒   ⊢ (Disj 𝑖 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (∪ 𝑥 ∈ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ 𝐷 𝐸) = ∅))
Theorem	disjiund 5065*	Conditions for a collection of index unions of sets 𝐴(𝑎, 𝑏) for 𝑎 ∈ 𝑉 and 𝑏 ∈ 𝑊 to be disjoint. (Contributed by AV, 9-Jan-2022.)
⊢ (𝑎 = 𝑐 → 𝐴 = 𝐶)    &   ⊢ (𝑏 = 𝑑 → 𝐶 = 𝐷)    &   ⊢ (𝑎 = 𝑐 → 𝑊 = 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐷) → 𝑎 = 𝑐)    ⇒   ⊢ (𝜑 → Disj 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ 𝑊 𝐴)
Theorem	sndisj 5066	Any collection of singletons is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ 𝐴 {𝑥}
Theorem	0disj 5067	Any collection of empty sets is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ 𝐴 ∅
Theorem	disjxsn 5068*	A singleton collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ {𝐴}𝐵
Theorem	disjx0 5069	An empty collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ 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 𝑥 ∈ 𝐵 𝐶))
2.1.23  Binary relations
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 11367.)
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 11173 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 30489). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5627, and in particular 𝑅 may be a function (see df-fun 6489). 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 7851). (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.)
⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)