P. 50 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4901-5000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pwpr 4901	The power set of an unordered pair. (Contributed by NM, 1-May-2009.)
⊢ 𝒫 {𝐴, 𝐵} = ({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}})
Theorem	pwtp 4902	The power set of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016.)
⊢ 𝒫 {𝐴, 𝐵, 𝐶} = (({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}}) ∪ ({{𝐶}, {𝐴, 𝐶}} ∪ {{𝐵, 𝐶}, {𝐴, 𝐵, 𝐶}}))
Theorem	pwpwpw0 4903	Compute the power set of the power set of the power set of the empty set. (See also pw0 4812 and pwpw0 4813.) (Contributed by NM, 2-May-2009.)
⊢ 𝒫 {∅, {∅}} = ({∅, {∅}} ∪ {{{∅}}, {∅, {∅}}})
Theorem	pwv 4904	The power class of the universe is the universe. Exercise 4.12(d) of [Mendelson] p. 235. The collection of all classes is of course larger than V, which is the collection of all sets. But 𝒫 V, being a class, cannot contain proper classes, so 𝒫 V is actually no larger than V. This fact is exploited in ncanth 7386. (Contributed by NM, 14-Sep-2003.)
⊢ 𝒫 V = V
Theorem	prproe 4905*	For an element of a proper unordered pair of elements of a class 𝑉, there is another (different) element of the class 𝑉 which is an element of the proper pair. (Contributed by AV, 18-Dec-2021.)
⊢ ((𝐶 ∈ {𝐴, 𝐵} ∧ 𝐴 ≠ 𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ∃𝑣 ∈ (𝑉 ∖ {𝐶})𝑣 ∈ {𝐴, 𝐵})
Theorem	3elpr2eq 4906	If there are three elements in a proper unordered pair, and two of them are different from the third one, the two must be equal. (Contributed by AV, 19-Dec-2021.)
⊢ (((𝑋 ∈ {𝐴, 𝐵} ∧ 𝑌 ∈ {𝐴, 𝐵} ∧ 𝑍 ∈ {𝐴, 𝐵}) ∧ (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋)) → 𝑌 = 𝑍)
2.1.19  The union of a class
Syntax	cuni 4907	Extend class notation to include the union of a class. Read: "union (of) 𝐴".
class ∪ 𝐴
Definition	df-uni 4908*	Define the union of a class i.e. the collection of all members of the members of the class. Definition 5.5 of [TakeutiZaring] p. 16. For example, ∪ {{1, 3}, {1, 8}} = {1, 3, 8} (ex-uni 30445). This is similar to the union of two classes df-un 3956. (Contributed by NM, 23-Aug-1993.)
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)}
Theorem	dfuni2 4909*	Alternate definition of class union. (Contributed by NM, 28-Jun-1998.)
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦}
Theorem	eluni 4910*	Membership in class union. (Contributed by NM, 22-May-1994.)
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
Theorem	eluni2 4911*	Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.)
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)
Theorem	elunii 4912	Membership in class union. (Contributed by NM, 24-Mar-1995.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)
Theorem	nfunid 4913	Deduction version of nfuni 4914. (Contributed by NM, 18-Feb-2013.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴)
Theorem	nfuni 4914	Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥∪ 𝐴
Theorem	uniss 4915	Subclass relationship for class union. Theorem 61 of [Suppes] p. 39. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
Theorem	unissi 4916	Subclass relationship for subclass union. Inference form of uniss 4915. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ∪ 𝐴 ⊆ ∪ 𝐵
Theorem	unissd 4917	Subclass relationship for subclass union. Deduction form of uniss 4915. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵)
Theorem	unieq 4918	Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18. (Contributed by NM, 10-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by BJ, 13-Apr-2024.)
⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
Theorem	unieqi 4919	Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∪ 𝐴 = ∪ 𝐵
Theorem	unieqd 4920	Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵)
Theorem	eluniab 4921*	Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.)
⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑))
Theorem	elunirab 4922*	Membership in union of a class abstraction. (Contributed by NM, 4-Oct-2006.)
⊢ (𝐴 ∈ ∪ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝜑))
Theorem	uniprg 4923	The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 25-Aug-2006.) Avoid using unipr 4924 to prove it from uniprg 4923. (Revised by BJ, 1-Sep-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))
Theorem	unipr 4924	The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 23-Aug-1993.) (Proof shortened by BJ, 1-Sep-2024.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)
Theorem	unisng 4925	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 13-Aug-2002.)
⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)
Theorem	unisn 4926	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∪ {𝐴} = 𝐴
Theorem	unisnv 4927	A set equals the union of its singleton (setvar case). (Contributed by NM, 30-Aug-1993.)
⊢ ∪ {𝑥} = 𝑥
Theorem	unisn3 4928*	Union of a singleton in the form of a restricted class abstraction. (Contributed by NM, 3-Jul-2008.)
⊢ (𝐴 ∈ 𝐵 → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 = 𝐴} = 𝐴)
Theorem	dfnfc2 4929*	An alternative statement of the effective freeness of a class 𝐴, when it is a set. (Contributed by Mario Carneiro, 14-Oct-2016.) (Proof shortened by JJ, 26-Jul-2021.)
⊢ (∀𝑥 𝐴 ∈ 𝑉 → (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴))
Theorem	uniun 4930	The class union of the union of two classes. Theorem 8.3 of [Quine] p. 53. (Contributed by NM, 20-Aug-1993.)
⊢ ∪ (𝐴 ∪ 𝐵) = (∪ 𝐴 ∪ ∪ 𝐵)
Theorem	uniin 4931	The class union of the intersection of two classes. Exercise 4.12(n) of [Mendelson] p. 235. See uniinqs 8837 for a condition where equality holds. (Contributed by NM, 4-Dec-2003.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ ∪ (𝐴 ∩ 𝐵) ⊆ (∪ 𝐴 ∩ ∪ 𝐵)
Theorem	ssuni 4932	Subclass relationship for class union. (Contributed by NM, 24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 26-Jul-2021.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ⊆ ∪ 𝐶)
Theorem	uni0b 4933	The union of a set is empty iff the set is included in the singleton of the empty set. (Contributed by NM, 12-Sep-2004.)
⊢ (∪ 𝐴 = ∅ ↔ 𝐴 ⊆ {∅})
Theorem	uni0c 4934*	The union of a set is empty iff all of its members are empty. (Contributed by NM, 16-Aug-2006.)
⊢ (∪ 𝐴 = ∅ ↔ ∀𝑥 ∈ 𝐴 𝑥 = ∅)
Theorem	uni0 4935	The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Contributed by NM, 16-Sep-1993.) Remove use of ax-nul 5306. (Revised by Eric Schmidt, 4-Apr-2007.)
⊢ ∪ ∅ = ∅
Theorem	csbuni 4936	Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012.) (Revised by NM, 22-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌∪ 𝐵 = ∪ ⦋𝐴 / 𝑥⦌𝐵
Theorem	elssuni 4937	An element of a class is a subclass of its union. Theorem 8.6 of [Quine] p. 54. Also the basis for Proposition 7.20 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Jun-1994.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ⊆ ∪ 𝐵)
Theorem	unissel 4938	Condition turning a subclass relationship for union into an equality. (Contributed by NM, 18-Jul-2006.)
⊢ ((∪ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐴) → ∪ 𝐴 = 𝐵)
Theorem	unissb 4939*	Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.) Avoid ax-11 2157. (Revised by BTernaryTau, 28-Dec-2024.)
⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
Theorem	unissbOLD 4940*	Obsolete version of unissb 4939 as of 28-Dec-2024. (Contributed by NM, 20-Sep-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
Theorem	uniss2 4941*	A subclass condition on the members of two classes that implies a subclass relation on their unions. Proposition 8.6 of [TakeutiZaring] p. 59. See iunss2 5049 for a generalization to indexed unions. (Contributed by NM, 22-Mar-2004.)
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∪ 𝐴 ⊆ ∪ 𝐵)
Theorem	unidif 4942*	If the difference 𝐴 ∖ 𝐵 contains the largest members of 𝐴, then the union of the difference is the union of 𝐴. (Contributed by NM, 22-Mar-2004.)
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ (𝐴 ∖ 𝐵)𝑥 ⊆ 𝑦 → ∪ (𝐴 ∖ 𝐵) = ∪ 𝐴)
Theorem	ssunieq 4943*	Relationship implying union. (Contributed by NM, 10-Nov-1999.)
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝑥 ⊆ 𝐴) → 𝐴 = ∪ 𝐵)
Theorem	unimax 4944*	Any member of a class is the largest of those members that it includes. (Contributed by NM, 13-Aug-2002.)
⊢ (𝐴 ∈ 𝐵 → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} = 𝐴)
Theorem	pwuni 4945	A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.)
⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴
2.1.20  The intersection of a class
Syntax	cint 4946	Extend class notation to include the intersection of a class. Read: "intersection (of) 𝐴".
class ∩ 𝐴
Definition	df-int 4947*	Define the intersection of a class. Definition 7.35 of [TakeutiZaring] p. 44. For example, ∩ {{1, 3}, {1, 8}} = {1}. Compare this with the intersection of two classes, df-in 3958. (Contributed by NM, 18-Aug-1993.)
⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦)}
Theorem	dfint2 4948*	Alternate definition of class intersection. (Contributed by NM, 28-Jun-1998.)
⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦}
Theorem	inteq 4949	Equality law for intersection. (Contributed by NM, 13-Sep-1999.)
⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)
Theorem	inteqi 4950	Equality inference for class intersection. (Contributed by NM, 2-Sep-2003.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∩ 𝐴 = ∩ 𝐵
Theorem	inteqd 4951	Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵)
Theorem	elint 4952*	Membership in class intersection. (Contributed by NM, 21-May-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥))
Theorem	elint2 4953*	Membership in class intersection. (Contributed by NM, 14-Oct-1999.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)
Theorem	elintg 4954*	Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003.) (Proof shortened by JJ, 26-Jul-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥))
Theorem	elinti 4955	Membership in class intersection. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (𝐴 ∈ ∩ 𝐵 → (𝐶 ∈ 𝐵 → 𝐴 ∈ 𝐶))
Theorem	nfint 4956	Bound-variable hypothesis builder for intersection. (Contributed by NM, 2-Feb-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥∩ 𝐴
Theorem	elintabg 4957*	Two ways of saying a set is an element of the intersection of a class. (Contributed by NM, 30-Aug-1993.) Put in closed form. (Revised by RP, 13-Aug-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)))
Theorem	elintab 4958*	Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))
Theorem	elintabOLD 4959*	Obsolete version of elintab 4958 as of 17-Jan-2025. (Contributed by NM, 30-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))
Theorem	elintrab 4960*	Membership in the intersection of a class abstraction. (Contributed by NM, 17-Oct-1999.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥))
Theorem	elintrabg 4961*	Membership in the intersection of a class abstraction. (Contributed by NM, 17-Feb-2007.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥)))
Theorem	int0 4962	The intersection of the empty set is the universal class. Exercise 2 of [TakeutiZaring] p. 44. (Contributed by NM, 18-Aug-1993.) (Proof shortened by JJ, 26-Jul-2021.)
⊢ ∩ ∅ = V
Theorem	intss1 4963	An element of a class includes the intersection of the class. Exercise 4 of [TakeutiZaring] p. 44 (with correction), generalized to classes. (Contributed by NM, 18-Nov-1995.)
⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)
Theorem	ssint 4964*	Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52 and its converse. (Contributed by NM, 14-Oct-1999.)
⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥)
Theorem	ssintab 4965*	Subclass of the intersection of a class abstraction. (Contributed by NM, 31-Jul-2006.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (𝐴 ⊆ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ⊆ 𝑥))
Theorem	ssintub 4966*	Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.)
⊢ 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}
Theorem	ssmin 4967*	Subclass of the minimum value of class of supersets. (Contributed by NM, 10-Aug-2006.)
⊢ 𝐴 ⊆ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)}
Theorem	intmin 4968*	Any member of a class is the smallest of those members that include it. (Contributed by NM, 13-Aug-2002.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (𝐴 ∈ 𝐵 → ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} = 𝐴)
Theorem	intss 4969	Intersection of subclasses. (Contributed by NM, 14-Oct-1999.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ (𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴)
Theorem	intssuni 4970	The intersection of a nonempty set is a subclass of its union. (Contributed by NM, 29-Jul-2006.)
⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)
Theorem	ssintrab 4971*	Subclass of the intersection of a restricted class abstraction. (Contributed by NM, 30-Jan-2015.)
⊢ (𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ⊆ 𝑥))
Theorem	unissint 4972	If the union of a class is included in its intersection, the class is either the empty set or a singleton (uniintsn 4985). (Contributed by NM, 30-Oct-2010.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∪ 𝐴 ⊆ ∩ 𝐴 ↔ (𝐴 = ∅ ∨ ∪ 𝐴 = ∩ 𝐴))
Theorem	intssuni2 4973	Subclass relationship for intersection and union. (Contributed by NM, 29-Jul-2006.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ⊆ ∪ 𝐵)
Theorem	intminss 4974*	Under subset ordering, the intersection of a restricted class abstraction is less than or equal to any of its members. (Contributed by NM, 7-Sep-2013.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ⊆ 𝐴)
Theorem	intmin2 4975*	Any set is the smallest of all sets that include it. (Contributed by NM, 20-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ 𝐴 ⊆ 𝑥} = 𝐴
Theorem	intmin3 4976*	Under subset ordering, the intersection of a class abstraction is less than or equal to any of its members. (Contributed by NM, 3-Jul-2005.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜓    ⇒   ⊢ (𝐴 ∈ 𝑉 → ∩ {𝑥 ∣ 𝜑} ⊆ 𝐴)
Theorem	intmin4 4977*	Elimination of a conjunct in a class intersection. (Contributed by NM, 31-Jul-2006.)
⊢ (𝐴 ⊆ ∩ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)} = ∩ {𝑥 ∣ 𝜑})
Theorem	intab 4978*	The intersection of a special case of a class abstraction. 𝑦 may be free in 𝜑 and 𝐴, which can be thought of a 𝜑(𝑦) and 𝐴(𝑦). Typically, abrexex2 7994 or abexssex 7995 can be used to satisfy the second hypothesis. (Contributed by NM, 28-Jul-2006.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
⊢ 𝐴 ∈ V    &   ⊢ {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)}
Theorem	int0el 4979	The intersection of a class containing the empty set is empty. (Contributed by NM, 24-Apr-2004.)
⊢ (∅ ∈ 𝐴 → ∩ 𝐴 = ∅)
Theorem	intun 4980	The class intersection of the union of two classes. Theorem 78 of [Suppes] p. 42. (Contributed by NM, 22-Sep-2002.)
⊢ ∩ (𝐴 ∪ 𝐵) = (∩ 𝐴 ∩ ∩ 𝐵)
Theorem	intprg 4981	The intersection of a pair is the intersection of its members. Closed form of intpr 4982. Theorem 71 of [Suppes] p. 42. (Contributed by FL, 27-Apr-2008.) (Proof shortened by BJ, 1-Sep-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵))
Theorem	intpr 4982	The intersection of a pair is the intersection of its members. Theorem 71 of [Suppes] p. 42. (Contributed by NM, 14-Oct-1999.) Prove from intprg 4981. (Revised by BJ, 1-Sep-2024.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵)
Theorem	intsng 4983	Intersection of a singleton. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝐴 ∈ 𝑉 → ∩ {𝐴} = 𝐴)
Theorem	intsn 4984	The intersection of a singleton is its member. Theorem 70 of [Suppes] p. 41. (Contributed by NM, 29-Sep-2002.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝐴} = 𝐴
Theorem	uniintsn 4985*	Two ways to express "𝐴 is a singleton". See also en1 9064, en1b 9065, card1 10008, and eusn 4730. (Contributed by NM, 2-Aug-2010.)
⊢ (∪ 𝐴 = ∩ 𝐴 ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	uniintab 4986	The union and the intersection of a class abstraction are equal exactly when there is a unique satisfying value of 𝜑(𝑥). (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (∃!𝑥𝜑 ↔ ∪ {𝑥 ∣ 𝜑} = ∩ {𝑥 ∣ 𝜑})
Theorem	intunsn 4987	Theorem joining a singleton to an intersection. (Contributed by NM, 29-Sep-2002.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ (𝐴 ∪ {𝐵}) = (∩ 𝐴 ∩ 𝐵)
Theorem	rint0 4988	Relative intersection of an empty set. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 = ∅ → (𝐴 ∩ ∩ 𝑋) = 𝐴)
Theorem	elrint 4989*	Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 ∈ (𝐴 ∩ ∩ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 𝑋 ∈ 𝑦))
Theorem	elrint2 4990*	Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 ∈ 𝐴 → (𝑋 ∈ (𝐴 ∩ ∩ 𝐵) ↔ ∀𝑦 ∈ 𝐵 𝑋 ∈ 𝑦))
2.1.21  Indexed union and intersection
Syntax	ciun 4991	Extend class notation to include indexed union. Note: Historically (prior to 21-Oct-2005), set.mm used the notation ∪ 𝑥 ∈ 𝐴𝐵, with the same union symbol as cuni 4907. While that syntax was unambiguous, it did not allow for LALR parsing of the syntax constructions in set.mm. The new syntax uses a distinguished symbol ∪ instead of ∪ and does allow LALR parsing. Thanks to Peter Backes for suggesting this change.
class ∪ 𝑥 ∈ 𝐴 𝐵
Syntax	ciin 4992	Extend class notation to include indexed intersection. Note: Historically (prior to 21-Oct-2005), set.mm used the notation ∩ 𝑥 ∈ 𝐴𝐵, with the same intersection symbol as cint 4946. Although that syntax was unambiguous, it did not allow for LALR parsing of the syntax constructions in set.mm. The new syntax uses a distinguished symbol ∩ instead of ∩ and does allow LALR parsing. Thanks to Peter Backes for suggesting this change.
class ∩ 𝑥 ∈ 𝐴 𝐵
Definition	df-iun 4993*	Define indexed union. Definition indexed union in [Stoll] p. 45. In most applications, 𝐴 is independent of 𝑥 (although this is not required by the definition), and 𝐵 depends on 𝑥 i.e. can be read informally as 𝐵(𝑥). We call 𝑥 the index, 𝐴 the index set, and 𝐵 the indexed set. In most books, 𝑥 ∈ 𝐴 is written as a subscript or underneath a union symbol ∪. We use a special union symbol ∪ to make it easier to distinguish from plain class union. In many theorems, you will see that 𝑥 and 𝐴 are in the same distinct variable group (meaning 𝐴 cannot depend on 𝑥) and that 𝐵 and 𝑥 do not share a distinct variable group (meaning that can be thought of as 𝐵(𝑥) i.e. can be substituted with a class expression containing 𝑥). An alternate definition tying indexed union to ordinary union is dfiun2 5033. Theorem uniiun 5058 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7267 and funiunfv 7268 are useful when 𝐵 is a function. (Contributed by NM, 27-Jun-1998.)
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
Definition	df-iin 4994*	Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 4993. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 5034. Theorem intiin 5059 provides a definition of ordinary intersection in terms of indexed intersection. (Contributed by NM, 27-Jun-1998.)
⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
Theorem	eliun 4995*	Membership in indexed union. (Contributed by NM, 3-Sep-2003.)
⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)
Theorem	eliin 4996*	Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
Theorem	eliuni 4997*	Membership in an indexed union, one way. (Contributed by JJ, 27-Jul-2021.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ 𝐶) → 𝐸 ∈ ∪ 𝑥 ∈ 𝐷 𝐵)
Theorem	eliund 4998*	Membership in indexed union. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	iuncom 4999*	Commutation of indexed unions. (Contributed by NM, 18-Dec-2008.)
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = ∪ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶
Theorem	iuncom4 5000	Commutation of union with indexed union. (Contributed by Mario Carneiro, 18-Jan-2014.)
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝐵 = ∪ ∪ 𝑥 ∈ 𝐴 𝐵