P. 40 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3901-4000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nfiunya 3901*	Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵
Theorem	nfiinya 3902*	Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵
Theorem	nfiu1 3903	Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.)
⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
Theorem	nfii1 3904	Bound-variable hypothesis builder for indexed intersection. (Contributed by NM, 15-Oct-2003.)
⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵
Theorem	dfiun2g 3905*	Alternate definition of indexed union when 𝐵 is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
Theorem	dfiin2g 3906*	Alternate definition of indexed intersection when 𝐵 is a set. (Contributed by Jeff Hankins, 27-Aug-2009.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
Theorem	dfiun2 3907*	Alternate definition of indexed union when 𝐵 is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 27-Jun-1998.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}
Theorem	dfiin2 3908*	Alternate definition of indexed intersection when 𝐵 is a set. Definition 15(b) of [Suppes] p. 44. (Contributed by NM, 28-Jun-1998.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}
Theorem	dfiunv2 3909*	Define double indexed union. (Contributed by FL, 6-Nov-2013.)
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 ∈ 𝐶}
Theorem	cbviun 3910*	Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 26-Mar-2006.) (Revised by Andrew Salmon, 25-Jul-2011.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶
Theorem	cbviin 3911*	Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶
Theorem	cbviunv 3912*	Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 15-Sep-2003.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶
Theorem	cbviinv 3913*	Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶
Theorem	iunss 3914*	Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	ssiun 3915*	Subset implication for an indexed union. (Contributed by NM, 3-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∃𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	ssiun2 3916	Identity law for subset of an indexed union. (Contributed by NM, 12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	ssiun2s 3917*	Subset relationship for an indexed union. (Contributed by NM, 26-Oct-2003.)
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)    ⇒   ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	iunss2 3918*	A subclass condition on the members of two indexed classes 𝐶(𝑥) and 𝐷(𝑦) that implies a subclass relation on their indexed unions. Generalization of Proposition 8.6 of [TakeutiZaring] p. 59. Compare uniss2 3827. (Contributed by NM, 9-Dec-2004.)
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 ⊆ 𝐷 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑦 ∈ 𝐵 𝐷)
Theorem	iunab 3919*	The indexed union of a class abstraction. (Contributed by NM, 27-Dec-2004.)
⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑}
Theorem	iunrab 3920*	The indexed union of a restricted class abstraction. (Contributed by NM, 3-Jan-2004.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝐴 𝜑}
Theorem	iunxdif2 3921*	Indexed union with a class difference as its index. (Contributed by NM, 10-Dec-2004.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ (𝐴 ∖ 𝐵)𝐶 ⊆ 𝐷 → ∪ 𝑦 ∈ (𝐴 ∖ 𝐵)𝐷 = ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	ssiinf 3922	Subset theorem for an indexed intersection. (Contributed by FL, 15-Oct-2012.) (Proof shortened by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵)
Theorem	ssiin 3923*	Subset theorem for an indexed intersection. (Contributed by NM, 15-Oct-2003.)
⊢ (𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵)
Theorem	iinss 3924*	Subset implication for an indexed intersection. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	iinss2 3925	An indexed intersection is included in any of its members. (Contributed by FL, 15-Oct-2012.)
⊢ (𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵)
Theorem	uniiun 3926*	Class union in terms of indexed union. Definition in [Stoll] p. 43. (Contributed by NM, 28-Jun-1998.)
⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥
Theorem	intiin 3927*	Class intersection in terms of indexed intersection. Definition in [Stoll] p. 44. (Contributed by NM, 28-Jun-1998.)
⊢ ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝑥
Theorem	iunid 3928*	An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.)
⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴
Theorem	iun0 3929	An indexed union of the empty set is empty. (Contributed by NM, 26-Mar-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ∪ 𝑥 ∈ 𝐴 ∅ = ∅
Theorem	0iun 3930	An empty indexed union is empty. (Contributed by NM, 4-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅
Theorem	0iin 3931	An empty indexed intersection is the universal class. (Contributed by NM, 20-Oct-2005.)
⊢ ∩ 𝑥 ∈ ∅ 𝐴 = V
Theorem	viin 3932*	Indexed intersection with a universal index class. (Contributed by NM, 11-Sep-2008.)
⊢ ∩ 𝑥 ∈ V 𝐴 = {𝑦 ∣ ∀𝑥 𝑦 ∈ 𝐴}
Theorem	iunn0m 3933*	There is an inhabited class in an indexed collection 𝐵(𝑥) iff the indexed union of them is inhabited. (Contributed by Jim Kingdon, 16-Aug-2018.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ 𝐵 ↔ ∃𝑦 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	iinab 3934*	Indexed intersection of a class builder. (Contributed by NM, 6-Dec-2011.)
⊢ ∩ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝜑}
Theorem	iinrabm 3935*	Indexed intersection of a restricted class builder. (Contributed by Jim Kingdon, 16-Aug-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑})
Theorem	iunin2 3936*	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 3926 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.)
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	iunin1 3937*	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 3926 to recover Enderton's theorem. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ ∪ 𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵) = (∪ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵)
Theorem	iundif2ss 3938*	Indexed union of class difference. Compare to theorem "De Morgan's laws" in [Enderton] p. 31. (Contributed by Jim Kingdon, 17-Aug-2018.)
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) ⊆ (𝐵 ∖ ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	2iunin 3939*	Rearrange indexed unions over intersection. (Contributed by NM, 18-Dec-2008.)
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 (𝐶 ∩ 𝐷) = (∪ 𝑥 ∈ 𝐴 𝐶 ∩ ∪ 𝑦 ∈ 𝐵 𝐷)
Theorem	iindif2m 3940*	Indexed intersection of class difference. Compare to Theorem "De Morgan's laws" in [Enderton] p. 31. (Contributed by Jim Kingdon, 17-Aug-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶))
Theorem	iinin2m 3941*	Indexed intersection of intersection. Compare to Theorem "Distributive laws" in [Enderton] p. 30. (Contributed by Jim Kingdon, 17-Aug-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶))
Theorem	iinin1m 3942*	Indexed intersection of intersection. Compare to Theorem "Distributive laws" in [Enderton] p. 30. (Contributed by Jim Kingdon, 17-Aug-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵) = (∩ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵))
Theorem	elriin 3943*	Elementhood in a relative intersection. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝐵 ∈ (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) ↔ (𝐵 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑆))
Theorem	riin0 3944*	Relative intersection of an empty family. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 = ∅ → (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) = 𝐴)
Theorem	riinm 3945*	Relative intersection of an inhabited family. (Contributed by Jim Kingdon, 19-Aug-2018.)
⊢ ((∀𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ ∃𝑥 𝑥 ∈ 𝑋) → (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) = ∩ 𝑥 ∈ 𝑋 𝑆)
Theorem	iinxsng 3946*	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 3947*	Indexed intersection with an unordered pair index. (Contributed by NM, 25-Jan-2012.)
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∩ 𝐸))
Theorem	iunxsng 3948*	A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶)
Theorem	iunxsn 3949*	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 3950*	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.)
⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶)
Theorem	iunun 3951	Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∪ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	iunxun 3952	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	iunxprg 3953*	A pair index picks out two instances of an indexed union's argument. (Contributed by Alexander van der Vekens, 2-Feb-2018.)
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∪ 𝐸))
Theorem	iunxiun 3954*	Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016.)
⊢ ∪ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 = ∪ 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶
Theorem	iinuniss 3955*	A relationship involving union and indexed intersection. Exercise 23 of [Enderton] p. 33 but with equality changed to subset. (Contributed by Jim Kingdon, 19-Aug-2018.)
⊢ (𝐴 ∪ ∩ 𝐵) ⊆ ∩ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥)
Theorem	iununir 3956*	A relationship involving union and indexed union. Exercise 25 of [Enderton] p. 33 but with biconditional changed to implication. (Contributed by Jim Kingdon, 19-Aug-2018.)
⊢ ((𝐴 ∪ ∪ 𝐵) = ∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) → (𝐵 = ∅ → 𝐴 = ∅))
Theorem	sspwuni 3957	Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)
Theorem	pwssb 3958*	Two ways to express a collection of subclasses. (Contributed by NM, 19-Jul-2006.)
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
Theorem	elpwpw 3959	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 3960*	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 3961*	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 3962	Relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
⊢ (𝐵 ∈ 𝐴 → (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 = 𝐵))
Theorem	iinpw 3963*	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 3964*	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	rintm 3965*	Relative intersection of an inhabited class. (Contributed by Jim Kingdon, 19-Aug-2018.)
⊢ ((𝑋 ⊆ 𝒫 𝐴 ∧ ∃𝑥 𝑥 ∈ 𝑋) → (𝐴 ∩ ∩ 𝑋) = ∩ 𝑋)
2.1.21  Disjointness
Syntax	wdisj 3966	Extend wff notation to include the statement that a family of classes 𝐵(𝑥), for 𝑥 ∈ 𝐴, is a disjoint family.
wff Disj 𝑥 ∈ 𝐴 𝐵
Definition	df-disj 3967*	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 3968*	Alternate definition for disjoint classes. (Contributed by NM, 17-Jun-2017.)
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
Theorem	disjss2 3969	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 3970	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑥 ∈ 𝐴 𝐶))
Theorem	disjeq2dv 3971*	Equality deduction for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑥 ∈ 𝐴 𝐶))
Theorem	disjss1 3972*	A subset of a disjoint collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶))
Theorem	disjeq1 3973*	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝐴 = 𝐵 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶))
Theorem	disjeq1d 3974*	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶))
Theorem	disjeq12d 3975*	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷))
Theorem	cbvdisj 3976*	Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶)
Theorem	cbvdisjv 3977*	Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 11-Dec-2016.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶)
Theorem	nfdisjv 3978*	Bound-variable hypothesis builder for disjoint collection. (Contributed by Jim Kingdon, 19-Aug-2018.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦Disj 𝑥 ∈ 𝐴 𝐵
Theorem	nfdisj1 3979	Bound-variable hypothesis builder for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Ⅎ𝑥Disj 𝑥 ∈ 𝐴 𝐵
Theorem	disjnim 3980*	If a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint, then pairs are disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Jim Kingdon, 6-Oct-2022.)
⊢ (𝑖 = 𝑗 → 𝐵 = 𝐶)    ⇒   ⊢ (Disj 𝑖 ∈ 𝐴 𝐵 → ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 ≠ 𝑗 → (𝐵 ∩ 𝐶) = ∅))
Theorem	disjnims 3981*	If a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint, then pairs are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by Jim Kingdon, 7-Oct-2022.)
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 ≠ 𝑗 → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
Theorem	disji2 3982*	Property of a disjoint collection: if 𝐵(𝑋) = 𝐶 and 𝐵(𝑌) = 𝐷, and 𝑋 ≠ 𝑌, then 𝐶 and 𝐷 are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)    &   ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷)    ⇒   ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝑋 ≠ 𝑌) → (𝐶 ∩ 𝐷) = ∅)
Theorem	invdisj 3983*	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	disjiun 3984*	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	sndisj 3985	Any collection of singletons is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ 𝐴 {𝑥}
Theorem	0disj 3986	Any collection of empty sets is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ 𝐴 ∅
Theorem	disjxsn 3987*	A singleton collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ {𝐴}𝐵
Theorem	disjx0 3988	An empty collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Disj 𝑥 ∈ ∅ 𝐵
2.1.22  Binary relations
Syntax	wbr 3989	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.
wff 𝐴𝑅𝐵
Definition	df-br 3990	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. 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 4879). (Contributed by NM, 31-Dec-1993.)
⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Theorem	breq 3991	Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.)
⊢ (𝑅 = 𝑆 → (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵))
Theorem	breq1 3992	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
Theorem	breq2 3993	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))
Theorem	breq12 3994	Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
Theorem	breqi 3995	Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑆𝐵)
Theorem	breq1i 3996	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)
Theorem	breq2i 3997	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵)
Theorem	breq12i 3998	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)
Theorem	breq1d 3999	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
Theorem	breqd 4000	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))