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	iunconst 5001*	Indexed union of a constant class, i.e. where 𝐵 does not depend on 𝑥. (Contributed by NM, 5-Sep-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 ≠ ∅ → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐵)
Theorem	iinconst 5002*	Indexed intersection of a constant class, i.e. where 𝐵 does not depend on 𝑥. (Contributed by Mario Carneiro, 6-Feb-2015.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 = 𝐵)
Theorem	iuneqconst 5003*	Indexed union of identical classes. (Contributed by AV, 5-Mar-2024.)
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐶)
Theorem	iuniin 5004*	Law combining indexed union with indexed intersection. Eq. 14 in [KuratowskiMostowski] p. 109. This theorem also appears as the last example at http://en.wikipedia.org/wiki/Union%5F%28set%5Ftheory%29. (Contributed by NM, 17-Aug-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ∪ 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 ⊆ ∩ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶
Theorem	iinssiun 5005*	An indexed intersection is a subset of the corresponding indexed union. (Contributed by Thierry Arnoux, 31-Dec-2021.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	iunss1 5006*	Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	iinss1 5007*	Subclass theorem for indexed intersection. (Contributed by NM, 24-Jan-2012.)
⊢ (𝐴 ⊆ 𝐵 → ∩ 𝑥 ∈ 𝐵 𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	iuneq1 5008*	Equality theorem for indexed union. (Contributed by NM, 27-Jun-1998.)
⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	iineq1 5009*	Equality theorem for indexed intersection. (Contributed by NM, 27-Jun-1998.)
⊢ (𝐴 = 𝐵 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶)
Theorem	ss2iun 5010	Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	iuneq2 5011	Equality theorem for indexed union. (Contributed by NM, 22-Oct-2003.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	iineq2 5012	Equality theorem for indexed intersection. (Contributed by NM, 22-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	iuneq2i 5013	Equality inference for indexed union. (Contributed by NM, 22-Oct-2003.)
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶
Theorem	iineq2i 5014	Equality inference for indexed intersection. (Contributed by NM, 22-Oct-2003.)
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶
Theorem	iineq2d 5015	Equality deduction for indexed intersection. (Contributed by NM, 7-Dec-2011.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	iuneq2dv 5016*	Equality deduction for indexed union. (Contributed by NM, 3-Aug-2004.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	iineq2dv 5017*	Equality deduction for indexed intersection. (Contributed by NM, 3-Aug-2004.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	iuneq12df 5018	Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 31-Dec-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
Theorem	iuneq1d 5019*	Equality theorem for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	iuneq12dOLD 5020*	Obsolete version of iuneq12d 5021 as of 1-Sep-2025. (Contributed by Drahflow, 22-Oct-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
Theorem	iuneq12d 5021*	Equality deduction for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.) Remove DV conditions (Revised by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
Theorem	iuneq2d 5022*	Equality deduction for indexed union. (Contributed by Drahflow, 22-Oct-2015.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	nfiun 5023*	Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2377. See nfiung 5025 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵
Theorem	nfiin 5024*	Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2377. See nfiing 5026 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵
Theorem	nfiung 5025	Bound-variable hypothesis builder for indexed union. Usage of this theorem is discouraged because it depends on ax-13 2377. See nfiun 5023 for a version with more disjoint variable conditions, but not requiring ax-13 2377. (Contributed by Mario Carneiro, 25-Jan-2014.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵
Theorem	nfiing 5026	Bound-variable hypothesis builder for indexed intersection. Usage of this theorem is discouraged because it depends on ax-13 2377. See nfiin 5024 for a version with more disjoint variable conditions, but not requiring ax-13 2377. (Contributed by Mario Carneiro, 25-Jan-2014.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵
Theorem	nfiu1 5027	Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) Avoid ax-11 2157, ax-12 2177. (Revised by SN, 14-May-2025.)
⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
Theorem	nfiu1OLD 5028	Obsolete version of nfiu1 5027 as of 14-May-2025. (Contributed by NM, 12-Oct-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
Theorem	nfii1 5029	Bound-variable hypothesis builder for indexed intersection. (Contributed by NM, 15-Oct-2003.)
⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵
Theorem	dfiun2g 5030*	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.) (Proof shortened by Rohan Ridenour, 11-Aug-2023.) Avoid ax-10 2141, ax-12 2177. (Revised by SN, 11-Dec-2024.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
Theorem	dfiun2gOLD 5031*	Obsolete version of dfiun2g 5030 as of 11-Dec-2024. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof shortened by Rohan Ridenour, 11-Aug-2023.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
Theorem	dfiin2g 5032*	Alternate definition of indexed intersection when 𝐵 is a set. (Contributed by Jeff Hankins, 27-Aug-2009.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
Theorem	dfiun2 5033*	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 5034*	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 5035*	Define double indexed union. (Contributed by FL, 6-Nov-2013.)
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 ∈ 𝐶}
Theorem	cbviun 5036*	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.) Add disjoint variable condition to avoid ax-13 2377. See cbviung 5038 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶
Theorem	cbviin 5037*	Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.) Add disjoint variable condition to avoid ax-13 2377. See cbviing 5039 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶
Theorem	cbviung 5038*	Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. Usage of this theorem is discouraged because it depends on ax-13 2377. See cbviun 5036 for a version with more disjoint variable conditions, but not requiring ax-13 2377. (Contributed by NM, 26-Mar-2006.) (Revised by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶
Theorem	cbviing 5039*	Change bound variables in an indexed intersection. Usage of this theorem is discouraged because it depends on ax-13 2377. See cbviin 5037 for a version with more disjoint variable conditions, but not requiring ax-13 2377. (Contributed by Jeff Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶
Theorem	cbviunv 5040*	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.) Add disjoint variable condition to avoid ax-13 2377. See cbviunvg 5042 for a less restrictive version requiring more axioms. (Revised by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶
Theorem	cbviinv 5041*	Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.) Add disjoint variable condition to avoid ax-13 2377. See cbviinvg 5043 for a less restrictive version requiring more axioms. (Revised by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶
Theorem	cbviunvg 5042*	Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. Usage of this theorem is discouraged because it depends on ax-13 2377. Usage of the weaker cbviunv 5040 is preferred. (Contributed by NM, 15-Sep-2003.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶
Theorem	cbviinvg 5043*	Change bound variables in an indexed intersection. Usage of this theorem is discouraged because it depends on ax-13 2377. Usage of the weaker cbviinv 5041 is preferred. (Contributed by Jeff Hankins, 26-Aug-2009.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶
Theorem	iunssf 5044	Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	iunss 5045*	Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	ssiun 5046*	Subset implication for an indexed union. (Contributed by NM, 3-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∃𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	ssiun2 5047	Identity law for subset of an indexed union. (Contributed by NM, 12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	ssiun2s 5048*	Subset relationship for an indexed union. (Contributed by NM, 26-Oct-2003.)
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)    ⇒   ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	iunss2 5049*	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 4941. (Contributed by NM, 9-Dec-2004.)
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 ⊆ 𝐷 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑦 ∈ 𝐵 𝐷)
Theorem	iunssd 5050*	Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	iunab 5051*	The indexed union of a class abstraction. (Contributed by NM, 27-Dec-2004.)
⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑}
Theorem	iunrab 5052*	The indexed union of a restricted class abstraction. (Contributed by NM, 3-Jan-2004.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝐴 𝜑}
Theorem	iunxdif2 5053*	Indexed union with a class difference as its index. (Contributed by NM, 10-Dec-2004.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ (𝐴 ∖ 𝐵)𝐶 ⊆ 𝐷 → ∪ 𝑦 ∈ (𝐴 ∖ 𝐵)𝐷 = ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	ssiinf 5054	Subset theorem for an indexed intersection. (Contributed by FL, 15-Oct-2012.) (Proof shortened by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵)
Theorem	ssiin 5055*	Subset theorem for an indexed intersection. (Contributed by NM, 15-Oct-2003.)
⊢ (𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵)
Theorem	iinss 5056*	Subset implication for an indexed intersection. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	iinss2 5057	An indexed intersection is included in any of its members. (Contributed by FL, 15-Oct-2012.)
⊢ (𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵)
Theorem	uniiun 5058*	Class union in terms of indexed union. Definition in [Stoll] p. 43. (Contributed by NM, 28-Jun-1998.)
⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥
Theorem	intiin 5059*	Class intersection in terms of indexed intersection. Definition in [Stoll] p. 44. (Contributed by NM, 28-Jun-1998.)
⊢ ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝑥
Theorem	iunid 5060*	An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.) (Proof shortened by SN, 15-Jan-2025.)
⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴
Theorem	iunidOLD 5061*	Obsolete version of iunid 5060 as of 15-Jan-2025. (Contributed by NM, 6-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴
Theorem	iun0 5062	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 5063	An empty indexed union is empty. (Contributed by NM, 4-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅
Theorem	0iin 5064	An empty indexed intersection is the universal class. (Contributed by NM, 20-Oct-2005.)
⊢ ∩ 𝑥 ∈ ∅ 𝐴 = V
Theorem	viin 5065*	Indexed intersection with a universal index class. When 𝐴 doesn't depend on 𝑥, this evaluates to 𝐴 by 19.3 2202 and abid2 2879. When 𝐴 = 𝑥, this evaluates to ∅ by intiin 5059 and intv 5364. (Contributed by NM, 11-Sep-2008.)
⊢ ∩ 𝑥 ∈ V 𝐴 = {𝑦 ∣ ∀𝑥 𝑦 ∈ 𝐴}
Theorem	iunsn 5066*	Indexed union of a singleton. Compare dfiun2 5033 and rnmpt 5968. (Contributed by Steven Nguyen, 7-Jun-2023.)
⊢ ∪ 𝑥 ∈ 𝐴 {𝐵} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}
Theorem	iunn0 5067*	There is a nonempty class in an indexed collection 𝐵(𝑥) iff the indexed union of them is nonempty. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∃𝑥 ∈ 𝐴 𝐵 ≠ ∅ ↔ ∪ 𝑥 ∈ 𝐴 𝐵 ≠ ∅)
Theorem	iinab 5068*	Indexed intersection of a class abstraction. (Contributed by NM, 6-Dec-2011.)
⊢ ∩ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝜑}
Theorem	iinrab 5069*	Indexed intersection of a restricted class abstraction. (Contributed by NM, 6-Dec-2011.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑})
Theorem	iinrab2 5070*	Indexed intersection of a restricted class abstraction. (Contributed by NM, 6-Dec-2011.)
⊢ (∩ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} ∩ 𝐵) = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑}
Theorem	iunin2 5071*	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 5058 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.)
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	iunin1 5072*	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 5058 to recover Enderton's theorem. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ ∪ 𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵) = (∪ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵)
Theorem	iinun2 5073*	Indexed intersection of union. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 5059 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.)
⊢ ∩ 𝑥 ∈ 𝐴 (𝐵 ∪ 𝐶) = (𝐵 ∪ ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	iundif2 5074*	Indexed union of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use intiin 5059 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.)
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (𝐵 ∖ ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	iindif1 5075*	Indexed intersection of class difference with the subtrahend held constant. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (∩ 𝑥 ∈ 𝐴 𝐵 ∖ 𝐶))
Theorem	2iunin 5076*	Rearrange indexed unions over intersection. (Contributed by NM, 18-Dec-2008.)
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 (𝐶 ∩ 𝐷) = (∪ 𝑥 ∈ 𝐴 𝐶 ∩ ∪ 𝑦 ∈ 𝐵 𝐷)
Theorem	iindif2 5077*	Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use uniiun 5058 to recover Enderton's theorem. (Contributed by NM, 5-Oct-2006.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶))
Theorem	iinin2 5078*	Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 5059 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶))
Theorem	iinin1 5079*	Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 5059 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵) = (∩ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵))
Theorem	iinvdif 5080*	The indexed intersection of a complement. (Contributed by Gérard Lang, 5-Aug-2018.)
⊢ ∩ 𝑥 ∈ 𝐴 (V ∖ 𝐵) = (V ∖ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	elriin 5081*	Elementhood in a relative intersection. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝐵 ∈ (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) ↔ (𝐵 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑆))
Theorem	riin0 5082*	Relative intersection of an empty family. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 = ∅ → (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) = 𝐴)
Theorem	riinn0 5083*	Relative intersection of a nonempty family. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((∀𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ 𝑋 ≠ ∅) → (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆) = ∩ 𝑥 ∈ 𝑋 𝑆)
Theorem	riinrab 5084*	Relative intersection of a relative abstraction. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝐴 ∩ ∩ 𝑥 ∈ 𝑋 {𝑦 ∈ 𝐴 ∣ 𝜑}) = {𝑦 ∈ 𝐴 ∣ ∀𝑥 ∈ 𝑋 𝜑}
Theorem	symdif0 5085	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 5086	The symmetric difference with the universal class is the complement. (Contributed by Scott Fenton, 24-Apr-2012.)
⊢ (𝐴 △ V) = (V ∖ 𝐴)
Theorem	symdifid 5087	The symmetric difference of a class with itself is the empty class. (Contributed by Scott Fenton, 25-Apr-2012.)
⊢ (𝐴 △ 𝐴) = ∅
Theorem	iinxsng 5088*	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 5089*	Indexed intersection with an unordered pair index. (Contributed by NM, 25-Jan-2012.)
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∩ 𝐸))
Theorem	iunxsng 5090*	A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶)
Theorem	iunxsn 5091*	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 5092*	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 2377. (Revised by GG, 19-May-2023.)
⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶)
Theorem	iunun 5093	Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∪ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	iunxun 5094	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 5095*	An indexed union where some terms are the empty set. See iunxdif2 5053. (Contributed by Thierry Arnoux, 4-May-2020.)
⊢ Ⅎ𝑥𝐸    ⇒   ⊢ (∀𝑥 ∈ 𝐸 𝐵 = ∅ → ∪ 𝑥 ∈ (𝐴 ∖ 𝐸)𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	iunxprg 5096*	A pair index picks out two instances of an indexed union's argument. (Contributed by Alexander van der Vekens, 2-Feb-2018.)
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∪ 𝐸))
Theorem	iunxiun 5097*	Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016.)
⊢ ∪ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 = ∪ 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶
Theorem	iinuni 5098*	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 5099*	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 5100	Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)