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	oteq1d 3901	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐶, 𝐷⟩ = ⟨𝐵, 𝐶, 𝐷⟩)
Theorem	oteq2d 3902	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨𝐶, 𝐴, 𝐷⟩ = ⟨𝐶, 𝐵, 𝐷⟩)
Theorem	oteq3d 3903	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)
Theorem	oteq123d 3904	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐸 = 𝐹)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐶, 𝐸⟩ = ⟨𝐵, 𝐷, 𝐹⟩)
Theorem	nfop 3905	Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥⟨𝐴, 𝐵⟩
Theorem	nfopd 3906	Deduction version of bound-variable hypothesis builder nfop 3905. This shows how the deduction version of a not-free theorem such as nfop 3905 can be created from the corresponding not-free inference theorem. (Contributed by NM, 4-Feb-2008.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥⟨𝐴, 𝐵⟩)
Theorem	opid 3907	The ordered pair ⟨𝐴, 𝐴⟩ in Kuratowski's representation. (Contributed by FL, 28-Dec-2011.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ⟨𝐴, 𝐴⟩ = {{𝐴}}
Theorem	ralunsn 3908*	Restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)))
Theorem	2ralunsn 3909*	Double restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝐵 ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∪ {𝐵})∀𝑦 ∈ (𝐴 ∪ {𝐵})𝜑 ↔ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) ∧ (∀𝑦 ∈ 𝐴 𝜒 ∧ 𝜃))))
Theorem	opprc 3910	Expansion of an ordered pair when either member is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐴, 𝐵⟩ = ∅)
Theorem	opprc1 3911	Expansion of an ordered pair when the first member is a proper class. See also opprc 3910. (Contributed by NM, 10-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (¬ 𝐴 ∈ V → ⟨𝐴, 𝐵⟩ = ∅)
Theorem	opprc2 3912	Expansion of an ordered pair when the second member is a proper class. See also opprc 3910. (Contributed by NM, 15-Nov-1994.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (¬ 𝐵 ∈ V → ⟨𝐴, 𝐵⟩ = ∅)
Theorem	oprcl 3913	If an ordered pair has an element, then its arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐶 ∈ ⟨𝐴, 𝐵⟩ → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	pwsnss 3914	The power set of a singleton. (Contributed by Jim Kingdon, 12-Aug-2018.)
⊢ {∅, {𝐴}} ⊆ 𝒫 {𝐴}
Theorem	pwpw0ss 3915	Compute the power set of the power set of the empty set. (See pw0 3847 for the power set of the empty set.) Theorem 90 of [Suppes] p. 48 (but with subset in place of equality). (Contributed by Jim Kingdon, 12-Aug-2018.)
⊢ {∅, {∅}} ⊆ 𝒫 {∅}
Theorem	pwprss 3916	The power set of an unordered pair. (Contributed by Jim Kingdon, 13-Aug-2018.)
⊢ ({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}}) ⊆ 𝒫 {𝐴, 𝐵}
Theorem	pwtpss 3917	The power set of an unordered triple. (Contributed by Jim Kingdon, 13-Aug-2018.)
⊢ (({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}}) ∪ ({{𝐶}, {𝐴, 𝐶}} ∪ {{𝐵, 𝐶}, {𝐴, 𝐵, 𝐶}})) ⊆ 𝒫 {𝐴, 𝐵, 𝐶}
Theorem	pwpwpw0ss 3918	Compute the power set of the power set of the power set of the empty set. (See also pw0 3847 and pwpw0ss 3915.) (Contributed by Jim Kingdon, 13-Aug-2018.)
⊢ ({∅, {∅}} ∪ {{{∅}}, {∅, {∅}}}) ⊆ 𝒫 {∅, {∅}}
Theorem	pwv 3919	The power class of the universe is the universe. Exercise 4.12(d) of [Mendelson] p. 235. (Contributed by NM, 14-Sep-2003.)
⊢ 𝒫 V = V
2.1.18  The union of a class
Syntax	cuni 3920	Extend class notation to include the union of a class. Read: "union (of) 𝐴".
class ∪ 𝐴
Definition	df-uni 3921*	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}. This is similar to the union of two classes df-un 3218. (Contributed by NM, 23-Aug-1993.)
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)}
Theorem	dfuni2 3922*	Alternate definition of class union. (Contributed by NM, 28-Jun-1998.)
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦}
Theorem	eluni 3923*	Membership in class union. (Contributed by NM, 22-May-1994.)
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
Theorem	eluni2 3924*	Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.)
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)
Theorem	elunii 3925	Membership in class union. (Contributed by NM, 24-Mar-1995.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)
Theorem	nfuni 3926	Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥∪ 𝐴
Theorem	nfunid 3927	Deduction version of nfuni 3926. (Contributed by NM, 18-Feb-2013.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴)
Theorem	csbunig 3928	Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌∪ 𝐵 = ∪ ⦋𝐴 / 𝑥⦌𝐵)
Theorem	unieq 3929	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.)
⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
Theorem	unieqi 3930	Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∪ 𝐴 = ∪ 𝐵
Theorem	unieqd 3931	Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵)
Theorem	eluniab 3932*	Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.)
⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑))
Theorem	elunirab 3933*	Membership in union of a class abstraction. (Contributed by NM, 4-Oct-2006.)
⊢ (𝐴 ∈ ∪ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝜑))
Theorem	unipr 3934	The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 23-Aug-1993.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)
Theorem	uniprg 3935	The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 25-Aug-2006.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))
Theorem	unisn 3936	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∪ {𝐴} = 𝐴
Theorem	unisng 3937	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 13-Aug-2002.)
⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)
Theorem	dfnfc2 3938*	An alternate statement of the effective freeness of a class 𝐴, when it is a set. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ (∀𝑥 𝐴 ∈ 𝑉 → (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴))
Theorem	uniun 3939	The class union of the union of two classes. Theorem 8.3 of [Quine] p. 53. (Contributed by NM, 20-Aug-1993.)
⊢ ∪ (𝐴 ∪ 𝐵) = (∪ 𝐴 ∪ ∪ 𝐵)
Theorem	uniin 3940	The class union of the intersection of two classes. Exercise 4.12(n) of [Mendelson] p. 235. (Contributed by NM, 4-Dec-2003.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ ∪ (𝐴 ∩ 𝐵) ⊆ (∪ 𝐴 ∩ ∪ 𝐵)
Theorem	uniss 3941	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	ssuni 3942	Subclass relationship for class union. (Contributed by NM, 24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ⊆ ∪ 𝐶)
Theorem	unissi 3943	Subclass relationship for subclass union. Inference form of uniss 3941. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ∪ 𝐴 ⊆ ∪ 𝐵
Theorem	unissd 3944	Subclass relationship for subclass union. Deduction form of uniss 3941. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵)
Theorem	uni0b 3945	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 3946*	The union of a set is empty iff all of its members are empty. (Contributed by NM, 16-Aug-2006.)
⊢ (∪ 𝐴 = ∅ ↔ ∀𝑥 ∈ 𝐴 𝑥 = ∅)
Theorem	uni0 3947	The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul by Eric Schmidt.) (Contributed by NM, 16-Sep-1993.) (Revised by Eric Schmidt, 4-Apr-2007.)
⊢ ∪ ∅ = ∅
Theorem	elssuni 3948	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 3949	Condition turning a subclass relationship for union into an equality. (Contributed by NM, 18-Jul-2006.)
⊢ ((∪ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐴) → ∪ 𝐴 = 𝐵)
Theorem	unissb 3950*	Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.)
⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
Theorem	uniss2 3951*	A subclass condition on the members of two classes that implies a subclass relation on their unions. Proposition 8.6 of [TakeutiZaring] p. 59. (Contributed by NM, 22-Mar-2004.)
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∪ 𝐴 ⊆ ∪ 𝐵)
Theorem	unidif 3952*	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 3953*	Relationship implying union. (Contributed by NM, 10-Nov-1999.)
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝑥 ⊆ 𝐴) → 𝐴 = ∪ 𝐵)
Theorem	unimax 3954*	Any member of a class is the largest of those members that it includes. (Contributed by NM, 13-Aug-2002.)
⊢ (𝐴 ∈ 𝐵 → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} = 𝐴)
2.1.19  The intersection of a class
Syntax	cint 3955	Extend class notation to include the intersection of a class. Read: "intersection (of) 𝐴".
class ∩ 𝐴
Definition	df-int 3956*	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 3220. (Contributed by NM, 18-Aug-1993.)
⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦)}
Theorem	dfint2 3957*	Alternate definition of class intersection. (Contributed by NM, 28-Jun-1998.)
⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦}
Theorem	inteq 3958	Equality law for intersection. (Contributed by NM, 13-Sep-1999.)
⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)
Theorem	inteqi 3959	Equality inference for class intersection. (Contributed by NM, 2-Sep-2003.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∩ 𝐴 = ∩ 𝐵
Theorem	inteqd 3960	Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵)
Theorem	elint 3961*	Membership in class intersection. (Contributed by NM, 21-May-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥))
Theorem	elint2 3962*	Membership in class intersection. (Contributed by NM, 14-Oct-1999.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)
Theorem	elintg 3963*	Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥))
Theorem	elinti 3964	Membership in class intersection. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (𝐴 ∈ ∩ 𝐵 → (𝐶 ∈ 𝐵 → 𝐴 ∈ 𝐶))
Theorem	nfint 3965	Bound-variable hypothesis builder for intersection. (Contributed by NM, 2-Feb-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥∩ 𝐴
Theorem	elintab 3966*	Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))
Theorem	elintrab 3967*	Membership in the intersection of a class abstraction. (Contributed by NM, 17-Oct-1999.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥))
Theorem	elintrabg 3968*	Membership in the intersection of a class abstraction. (Contributed by NM, 17-Feb-2007.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥)))
Theorem	int0 3969	The intersection of the empty set is the universal class. Exercise 2 of [TakeutiZaring] p. 44. (Contributed by NM, 18-Aug-1993.)
⊢ ∩ ∅ = V
Theorem	intss1 3970	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 3971*	Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52 and its converse. (Contributed by NM, 14-Oct-1999.)
⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥)
Theorem	ssintab 3972*	Subclass of the intersection of a class abstraction. (Contributed by NM, 31-Jul-2006.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (𝐴 ⊆ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ⊆ 𝑥))
Theorem	ssintub 3973*	Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.)
⊢ 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}
Theorem	ssmin 3974*	Subclass of the minimum value of class of supersets. (Contributed by NM, 10-Aug-2006.)
⊢ 𝐴 ⊆ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)}
Theorem	intmin 3975*	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 3976	Intersection of subclasses. (Contributed by NM, 14-Oct-1999.)
⊢ (𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴)
Theorem	intssunim 3977*	The intersection of an inhabited set is a subclass of its union. (Contributed by NM, 29-Jul-2006.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ ∪ 𝐴)
Theorem	ssintrab 3978*	Subclass of the intersection of a restricted class builder. (Contributed by NM, 30-Jan-2015.)
⊢ (𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ⊆ 𝑥))
Theorem	intssuni2m 3979*	Subclass relationship for intersection and union. (Contributed by Jim Kingdon, 14-Aug-2018.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ⊆ ∪ 𝐵)
Theorem	intminss 3980*	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 3981*	Any set is the smallest of all sets that include it. (Contributed by NM, 20-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ 𝐴 ⊆ 𝑥} = 𝐴
Theorem	intmin3 3982*	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 3983*	Elimination of a conjunct in a class intersection. (Contributed by NM, 31-Jul-2006.)
⊢ (𝐴 ⊆ ∩ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)} = ∩ {𝑥 ∣ 𝜑})
Theorem	intab 3984*	The intersection of a special case of a class abstraction. 𝑦 may be free in 𝜑 and 𝐴, which can be thought of a 𝜑(𝑦) and 𝐴(𝑦). (Contributed by NM, 28-Jul-2006.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
⊢ 𝐴 ∈ V    &   ⊢ {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)}
Theorem	int0el 3985	The intersection of a class containing the empty set is empty. (Contributed by NM, 24-Apr-2004.)
⊢ (∅ ∈ 𝐴 → ∩ 𝐴 = ∅)
Theorem	intun 3986	The class intersection of the union of two classes. Theorem 78 of [Suppes] p. 42. (Contributed by NM, 22-Sep-2002.)
⊢ ∩ (𝐴 ∪ 𝐵) = (∩ 𝐴 ∩ ∩ 𝐵)
Theorem	intpr 3987	The intersection of a pair is the intersection of its members. Theorem 71 of [Suppes] p. 42. (Contributed by NM, 14-Oct-1999.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵)
Theorem	intprg 3988	The intersection of a pair is the intersection of its members. Closed form of intpr 3987. Theorem 71 of [Suppes] p. 42. (Contributed by FL, 27-Apr-2008.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵))
Theorem	intsng 3989	Intersection of a singleton. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝐴 ∈ 𝑉 → ∩ {𝐴} = 𝐴)
Theorem	intsn 3990	The intersection of a singleton is its member. Theorem 70 of [Suppes] p. 41. (Contributed by NM, 29-Sep-2002.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝐴} = 𝐴
Theorem	uniintsnr 3991*	The union and intersection of a singleton are equal. See also eusn 3771. (Contributed by Jim Kingdon, 14-Aug-2018.)
⊢ (∃𝑥 𝐴 = {𝑥} → ∪ 𝐴 = ∩ 𝐴)
Theorem	uniintabim 3992	The union and the intersection of a class abstraction are equal if there is a unique satisfying value of 𝜑(𝑥). (Contributed by Jim Kingdon, 14-Aug-2018.)
⊢ (∃!𝑥𝜑 → ∪ {𝑥 ∣ 𝜑} = ∩ {𝑥 ∣ 𝜑})
Theorem	intunsn 3993	Theorem joining a singleton to an intersection. (Contributed by NM, 29-Sep-2002.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ (𝐴 ∪ {𝐵}) = (∩ 𝐴 ∩ 𝐵)
Theorem	rint0 3994	Relative intersection of an empty set. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 = ∅ → (𝐴 ∩ ∩ 𝑋) = 𝐴)
Theorem	elrint 3995*	Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 ∈ (𝐴 ∩ ∩ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 𝑋 ∈ 𝑦))
Theorem	elrint2 3996*	Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 ∈ 𝐴 → (𝑋 ∈ (𝐴 ∩ ∩ 𝐵) ↔ ∀𝑦 ∈ 𝐵 𝑋 ∈ 𝑦))
2.1.20  Indexed union and intersection
Syntax	ciun 3997	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 3920. While that syntax was unambiguous, it did not allow for LALR parsing of the syntax constructions in set.mm. The new syntax uses as distinguished symbol ∪ instead of ∪ and does allow LALR parsing. Thanks to Peter Backes for suggesting this change.
class ∪ 𝑥 ∈ 𝐴 𝐵
Syntax	ciin 3998	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 3955. 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 3999*	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 disjoint variable group (meaning 𝐴 cannot depend on 𝑥) and that 𝐵 and 𝑥 do not share a disjoint 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 4031. Theorem uniiun 4051 provides a definition of ordinary union in terms of indexed union. (Contributed by NM, 27-Jun-1998.)
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
Definition	df-iin 4000*	Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3999. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 4032. Theorem intiin 4052 provides a definition of ordinary intersection in terms of indexed intersection. (Contributed by NM, 27-Jun-1998.)
⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}