P. 39 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3801-3900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eluniab 3801*	Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.)
⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑))
Theorem	elunirab 3802*	Membership in union of a class abstraction. (Contributed by NM, 4-Oct-2006.)
⊢ (𝐴 ∈ ∪ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝜑))
Theorem	unipr 3803	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 3804	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 3805	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∪ {𝐴} = 𝐴
Theorem	unisng 3806	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 13-Aug-2002.)
⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)
Theorem	dfnfc2 3807*	An alternate statement of the effective freeness of a class 𝐴, when it is a set. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ (∀𝑥 𝐴 ∈ 𝑉 → (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴))
Theorem	uniun 3808	The class union of the union of two classes. Theorem 8.3 of [Quine] p. 53. (Contributed by NM, 20-Aug-1993.)
⊢ ∪ (𝐴 ∪ 𝐵) = (∪ 𝐴 ∪ ∪ 𝐵)
Theorem	uniin 3809	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 3810	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 3811	Subclass relationship for class union. (Contributed by NM, 24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ⊆ ∪ 𝐶)
Theorem	unissi 3812	Subclass relationship for subclass union. Inference form of uniss 3810. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ∪ 𝐴 ⊆ ∪ 𝐵
Theorem	unissd 3813	Subclass relationship for subclass union. Deduction form of uniss 3810. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵)
Theorem	uni0b 3814	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 3815*	The union of a set is empty iff all of its members are empty. (Contributed by NM, 16-Aug-2006.)
⊢ (∪ 𝐴 = ∅ ↔ ∀𝑥 ∈ 𝐴 𝑥 = ∅)
Theorem	uni0 3816	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 3817	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 3818	Condition turning a subclass relationship for union into an equality. (Contributed by NM, 18-Jul-2006.)
⊢ ((∪ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐴) → ∪ 𝐴 = 𝐵)
Theorem	unissb 3819*	Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.)
⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
Theorem	uniss2 3820*	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 3821*	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 3822*	Relationship implying union. (Contributed by NM, 10-Nov-1999.)
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝑥 ⊆ 𝐴) → 𝐴 = ∪ 𝐵)
Theorem	unimax 3823*	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 3824	Extend class notation to include the intersection of a class. Read: "intersection (of) 𝐴".
class ∩ 𝐴
Definition	df-int 3825*	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 3122. (Contributed by NM, 18-Aug-1993.)
⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦)}
Theorem	dfint2 3826*	Alternate definition of class intersection. (Contributed by NM, 28-Jun-1998.)
⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦}
Theorem	inteq 3827	Equality law for intersection. (Contributed by NM, 13-Sep-1999.)
⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)
Theorem	inteqi 3828	Equality inference for class intersection. (Contributed by NM, 2-Sep-2003.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∩ 𝐴 = ∩ 𝐵
Theorem	inteqd 3829	Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵)
Theorem	elint 3830*	Membership in class intersection. (Contributed by NM, 21-May-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥))
Theorem	elint2 3831*	Membership in class intersection. (Contributed by NM, 14-Oct-1999.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)
Theorem	elintg 3832*	Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥))
Theorem	elinti 3833	Membership in class intersection. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (𝐴 ∈ ∩ 𝐵 → (𝐶 ∈ 𝐵 → 𝐴 ∈ 𝐶))
Theorem	nfint 3834	Bound-variable hypothesis builder for intersection. (Contributed by NM, 2-Feb-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥∩ 𝐴
Theorem	elintab 3835*	Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))
Theorem	elintrab 3836*	Membership in the intersection of a class abstraction. (Contributed by NM, 17-Oct-1999.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥))
Theorem	elintrabg 3837*	Membership in the intersection of a class abstraction. (Contributed by NM, 17-Feb-2007.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥)))
Theorem	int0 3838	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 3839	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 3840*	Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52 and its converse. (Contributed by NM, 14-Oct-1999.)
⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥)
Theorem	ssintab 3841*	Subclass of the intersection of a class abstraction. (Contributed by NM, 31-Jul-2006.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (𝐴 ⊆ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ⊆ 𝑥))
Theorem	ssintub 3842*	Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.)
⊢ 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}
Theorem	ssmin 3843*	Subclass of the minimum value of class of supersets. (Contributed by NM, 10-Aug-2006.)
⊢ 𝐴 ⊆ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)}
Theorem	intmin 3844*	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 3845	Intersection of subclasses. (Contributed by NM, 14-Oct-1999.)
⊢ (𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴)
Theorem	intssunim 3846*	The intersection of an inhabited set is a subclass of its union. (Contributed by NM, 29-Jul-2006.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ ∪ 𝐴)
Theorem	ssintrab 3847*	Subclass of the intersection of a restricted class builder. (Contributed by NM, 30-Jan-2015.)
⊢ (𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ⊆ 𝑥))
Theorem	intssuni2m 3848*	Subclass relationship for intersection and union. (Contributed by Jim Kingdon, 14-Aug-2018.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ⊆ ∪ 𝐵)
Theorem	intminss 3849*	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 3850*	Any set is the smallest of all sets that include it. (Contributed by NM, 20-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ 𝐴 ⊆ 𝑥} = 𝐴
Theorem	intmin3 3851*	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 3852*	Elimination of a conjunct in a class intersection. (Contributed by NM, 31-Jul-2006.)
⊢ (𝐴 ⊆ ∩ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)} = ∩ {𝑥 ∣ 𝜑})
Theorem	intab 3853*	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 3854	The intersection of a class containing the empty set is empty. (Contributed by NM, 24-Apr-2004.)
⊢ (∅ ∈ 𝐴 → ∩ 𝐴 = ∅)
Theorem	intun 3855	The class intersection of the union of two classes. Theorem 78 of [Suppes] p. 42. (Contributed by NM, 22-Sep-2002.)
⊢ ∩ (𝐴 ∪ 𝐵) = (∩ 𝐴 ∩ ∩ 𝐵)
Theorem	intpr 3856	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 3857	The intersection of a pair is the intersection of its members. Closed form of intpr 3856. Theorem 71 of [Suppes] p. 42. (Contributed by FL, 27-Apr-2008.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵))
Theorem	intsng 3858	Intersection of a singleton. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝐴 ∈ 𝑉 → ∩ {𝐴} = 𝐴)
Theorem	intsn 3859	The intersection of a singleton is its member. Theorem 70 of [Suppes] p. 41. (Contributed by NM, 29-Sep-2002.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝐴} = 𝐴
Theorem	uniintsnr 3860*	The union and intersection of a singleton are equal. See also eusn 3650. (Contributed by Jim Kingdon, 14-Aug-2018.)
⊢ (∃𝑥 𝐴 = {𝑥} → ∪ 𝐴 = ∩ 𝐴)
Theorem	uniintabim 3861	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 3862	Theorem joining a singleton to an intersection. (Contributed by NM, 29-Sep-2002.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ (𝐴 ∪ {𝐵}) = (∩ 𝐴 ∩ 𝐵)
Theorem	rint0 3863	Relative intersection of an empty set. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 = ∅ → (𝐴 ∩ ∩ 𝑋) = 𝐴)
Theorem	elrint 3864*	Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 ∈ (𝐴 ∩ ∩ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 𝑋 ∈ 𝑦))
Theorem	elrint2 3865*	Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 ∈ 𝐴 → (𝑋 ∈ (𝐴 ∩ ∩ 𝐵) ↔ ∀𝑦 ∈ 𝐵 𝑋 ∈ 𝑦))
2.1.20  Indexed union and intersection
Syntax	ciun 3866	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 3789. 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 3867	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 3824. 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 3868*	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 3900. Theorem uniiun 3919 provides a definition of ordinary union in terms of indexed union. (Contributed by NM, 27-Jun-1998.)
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
Definition	df-iin 3869*	Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3868. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 3901. Theorem intiin 3920 provides a definition of ordinary intersection in terms of indexed intersection. (Contributed by NM, 27-Jun-1998.)
⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
Theorem	eliun 3870*	Membership in indexed union. (Contributed by NM, 3-Sep-2003.)
⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)
Theorem	eliin 3871*	Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
Theorem	iuncom 3872*	Commutation of indexed unions. (Contributed by NM, 18-Dec-2008.)
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = ∪ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶
Theorem	iuncom4 3873	Commutation of union with indexed union. (Contributed by Mario Carneiro, 18-Jan-2014.)
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝐵 = ∪ ∪ 𝑥 ∈ 𝐴 𝐵
Theorem	iunconstm 3874*	Indexed union of a constant class, i.e. where 𝐵 does not depend on 𝑥. (Contributed by Jim Kingdon, 15-Aug-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐵)
Theorem	iinconstm 3875*	Indexed intersection of a constant class, i.e. where 𝐵 does not depend on 𝑥. (Contributed by Jim Kingdon, 19-Dec-2018.)
⊢ (∃𝑦 𝑦 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 𝐵 = 𝐵)
Theorem	iuniin 3876*	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	iunss1 3877*	Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	iinss1 3878*	Subclass theorem for indexed union. (Contributed by NM, 24-Jan-2012.)
⊢ (𝐴 ⊆ 𝐵 → ∩ 𝑥 ∈ 𝐵 𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	iuneq1 3879*	Equality theorem for indexed union. (Contributed by NM, 27-Jun-1998.)
⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	iineq1 3880*	Equality theorem for restricted existential quantifier. (Contributed by NM, 27-Jun-1998.)
⊢ (𝐴 = 𝐵 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶)
Theorem	ss2iun 3881	Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	iuneq2 3882	Equality theorem for indexed union. (Contributed by NM, 22-Oct-2003.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	iineq2 3883	Equality theorem for indexed intersection. (Contributed by NM, 22-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	iuneq2i 3884	Equality inference for indexed union. (Contributed by NM, 22-Oct-2003.)
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶
Theorem	iineq2i 3885	Equality inference for indexed intersection. (Contributed by NM, 22-Oct-2003.)
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶
Theorem	iineq2d 3886	Equality deduction for indexed intersection. (Contributed by NM, 7-Dec-2011.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	iuneq2dv 3887*	Equality deduction for indexed union. (Contributed by NM, 3-Aug-2004.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	iineq2dv 3888*	Equality deduction for indexed intersection. (Contributed by NM, 3-Aug-2004.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	iuneq1d 3889*	Equality theorem for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)
Theorem	iuneq12d 3890*	Equality deduction for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷)
Theorem	iuneq2d 3891*	Equality deduction for indexed union. (Contributed by Drahflow, 22-Oct-2015.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	nfiunxy 3892*	Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵
Theorem	nfiinxy 3893*	Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵
Theorem	nfiunya 3894*	Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵
Theorem	nfiinya 3895*	Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵
Theorem	nfiu1 3896	Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.)
⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
Theorem	nfii1 3897	Bound-variable hypothesis builder for indexed intersection. (Contributed by NM, 15-Oct-2003.)
⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵
Theorem	dfiun2g 3898*	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 3899*	Alternate definition of indexed intersection when 𝐵 is a set. (Contributed by Jeff Hankins, 27-Aug-2009.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
Theorem	dfiun2 3900*	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    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}