Type  Label  Description 
Statement 

Theorem  unieqi 3901 
Inference of equality of two class unions. (Contributed by NM,
30Aug1993.)

⊢ A =
B ⇒ ⊢ ∪A = ∪B 

Theorem  unieqd 3902 
Deduction of equality of two class unions. (Contributed by NM,
21Apr1995.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ ∪A =
∪B) 

Theorem  eluniab 3903* 
Membership in union of a class abstraction. (Contributed by NM,
11Aug1994.) (Revised by Mario Carneiro, 14Nov2016.)

⊢ (A ∈ ∪{x ∣ φ} ↔ ∃x(A ∈ x ∧ φ)) 

Theorem  elunirab 3904* 
Membership in union of a class abstraction. (Contributed by NM,
4Oct2006.)

⊢ (A ∈ ∪{x ∈ B ∣ φ} ↔ ∃x ∈ B (A ∈ x ∧ φ)) 

Theorem  unipr 3905 
The union of a pair is the union of its members. Proposition 5.7 of
[TakeutiZaring] p. 16.
(Contributed by NM, 23Aug1993.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ∪{A, B} =
(A ∪ B) 

Theorem  uniprg 3906 
The union of a pair is the union of its members. Proposition 5.7 of
[TakeutiZaring] p. 16.
(Contributed by NM, 25Aug2006.)

⊢ ((A ∈ V ∧ B ∈ W) →
∪{A, B} = (A ∪
B)) 

Theorem  unisn 3907 
A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
(Contributed by NM, 30Aug1993.)

⊢ A ∈ V ⇒ ⊢ ∪{A} = A 

Theorem  unisng 3908 
A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
(Contributed by NM, 13Aug2002.)

⊢ (A ∈ V →
∪{A} = A) 

Theorem  dfnfc2 3909* 
An alternative statement of the effective freeness of a class A,
when it is a set. (Contributed by Mario Carneiro, 14Oct2016.)

⊢ (∀x A ∈ V →
(F/_xA
↔ ∀yℲx
y = A)) 

Theorem  uniun 3910 
The class union of the union of two classes. Theorem 8.3 of [Quine]
p. 53. (Contributed by NM, 20Aug1993.)

⊢ ∪(A ∪ B) =
(∪A ∪ ∪B) 

Theorem  uniin 3911 
The class union of the intersection of two classes. Exercise 4.12(n) of
[Mendelson] p. 235. See uniinqs (future) for a condition where equality
holds. (Contributed by NM, 4Dec2003.) (Proof shortened by Andrew
Salmon, 29Jun2011.)

⊢ ∪(A ∩ B)
⊆ (∪A ∩ ∪B) 

Theorem  uniss 3912 
Subclass relationship for class union. Theorem 61 of [Suppes] p. 39.
(Contributed by NM, 22Mar1998.) (Proof shortened by Andrew Salmon,
29Jun2011.)

⊢ (A ⊆ B →
∪A ⊆ ∪B) 

Theorem  ssuni 3913 
Subclass relationship for class union. (Contributed by NM,
24May1994.) (Proof shortened by Andrew Salmon, 29Jun2011.)

⊢ ((A ⊆ B ∧ B ∈ C) →
A ⊆
∪C) 

Theorem  unissi 3914 
Subclass relationship for subclass union. Inference form of uniss 3912.
(Contributed by David Moews, 1May2017.)

⊢ A ⊆ B ⇒ ⊢ ∪A ⊆ ∪B 

Theorem  unissd 3915 
Subclass relationship for subclass union. Deduction form of uniss 3912.
(Contributed by David Moews, 1May2017.)

⊢ (φ
→ A ⊆ B) ⇒ ⊢ (φ
→ ∪A ⊆ ∪B) 

Theorem  uni0b 3916 
The union of a set is empty iff the set is included in the singleton of
the empty set. (Contributed by NM, 12Sep2004.)

⊢ (∪A = ∅ ↔
A ⊆
{∅}) 

Theorem  uni0c 3917* 
The union of a set is empty iff all of its members are empty.
(Contributed by NM, 16Aug2006.)

⊢ (∪A = ∅ ↔
∀x
∈ A
x = ∅) 

Theorem  uni0 3918 
The union of the empty set is the empty set. Theorem 8.7 of [Quine]
p. 54. (Reproved without relying on axnul (future) by Eric
Schmidt.)
(Contributed by NM, 16Sep1993.) (Revised by Eric Schmidt,
4Apr2007.)

⊢ ∪∅ = ∅ 

Theorem  elssuni 3919 
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, 6Jun1994.)

⊢ (A ∈ B →
A ⊆
∪B) 

Theorem  unissel 3920 
Condition turning a subclass relationship for union into an equality.
(Contributed by NM, 18Jul2006.)

⊢ ((∪A ⊆ B ∧ B ∈ A) → ∪A = B) 

Theorem  unissb 3921* 
Relationship involving membership, subset, and union. Exercise 5 of
[Enderton] p. 26 and its converse.
(Contributed by NM, 20Sep2003.)

⊢ (∪A ⊆ B ↔ ∀x ∈ A x ⊆ B) 

Theorem  uniss2 3922* 
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 4011 for a generalization to indexed unions.
(Contributed by NM, 22Mar2004.)

⊢ (∀x ∈ A ∃y ∈ B x ⊆ y →
∪A ⊆ ∪B) 

Theorem  unidif 3923* 
If the difference A ∖ B
contains the largest members of A, then
the union of the difference is the union of A. (Contributed by NM,
22Mar2004.)

⊢ (∀x ∈ A ∃y ∈ (A ∖ B)x ⊆ y →
∪(A ∖ B) = ∪A) 

Theorem  ssunieq 3924* 
Relationship implying union. (Contributed by NM, 10Nov1999.)

⊢ ((A ∈ B ∧ ∀x ∈ B x ⊆ A) →
A = ∪B) 

Theorem  unimax 3925* 
Any member of a class is the largest of those members that it includes.
(Contributed by NM, 13Aug2002.)

⊢ (A ∈ B →
∪{x ∈ B ∣ x ⊆ A} =
A) 

2.1.18 The intersection of a class


Syntax  cint 3926 
Extend class notation to include the intersection of a class (read:
'intersect A').

class
∩A 

Definition  dfint 3927* 
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, dfin 3213.
(Contributed by NM, 18Aug1993.)

⊢ ∩A = {x ∣ ∀y(y ∈ A →
x ∈
y)} 

Theorem  dfint2 3928* 
Alternate definition of class intersection. (Contributed by NM,
28Jun1998.)

⊢ ∩A = {x ∣ ∀y ∈ A x ∈ y} 

Theorem  inteq 3929 
Equality law for intersection. (Contributed by NM, 13Sep1999.)

⊢ (A =
B → ∩A = ∩B) 

Theorem  inteqi 3930 
Equality inference for class intersection. (Contributed by NM,
2Sep2003.)

⊢ A =
B ⇒ ⊢ ∩A = ∩B 

Theorem  inteqd 3931 
Equality deduction for class intersection. (Contributed by NM,
2Sep2003.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ ∩A =
∩B) 

Theorem  elint 3932* 
Membership in class intersection. (Contributed by NM, 21May1994.)

⊢ A ∈ V ⇒ ⊢ (A ∈ ∩B ↔ ∀x(x ∈ B → A
∈ x)) 

Theorem  elint2 3933* 
Membership in class intersection. (Contributed by NM, 14Oct1999.)

⊢ A ∈ V ⇒ ⊢ (A ∈ ∩B ↔ ∀x ∈ B A ∈ x) 

Theorem  elintg 3934* 
Membership in class intersection, with the sethood requirement expressed
as an antecedent. (Contributed by NM, 20Nov2003.)

⊢ (A ∈ V →
(A ∈
∩B ↔ ∀x ∈ B A ∈ x)) 

Theorem  elinti 3935 
Membership in class intersection. (Contributed by NM, 14Oct1999.)
(Proof shortened by Andrew Salmon, 9Jul2011.)

⊢ (A ∈ ∩B → (C
∈ B
→ A ∈ C)) 

Theorem  nfint 3936 
Boundvariable hypothesis builder for intersection. (Contributed by NM,
2Feb1997.) (Proof shortened by Andrew Salmon, 12Aug2011.)

⊢ F/_xA ⇒ ⊢ F/_x∩A 

Theorem  elintab 3937* 
Membership in the intersection of a class abstraction. (Contributed by
NM, 30Aug1993.)

⊢ A ∈ V ⇒ ⊢ (A ∈ ∩{x ∣ φ} ↔ ∀x(φ → A ∈ x)) 

Theorem  elintrab 3938* 
Membership in the intersection of a class abstraction. (Contributed by
NM, 17Oct1999.)

⊢ A ∈ V ⇒ ⊢ (A ∈ ∩{x ∈ B ∣ φ} ↔ ∀x ∈ B (φ → A ∈ x)) 

Theorem  elintrabg 3939* 
Membership in the intersection of a class abstraction. (Contributed by
NM, 17Feb2007.)

⊢ (A ∈ V →
(A ∈
∩{x ∈ B ∣ φ}
↔ ∀x ∈ B (φ →
A ∈
x))) 

Theorem  int0 3940 
The intersection of the empty set is the universal class. Exercise 2 of
[TakeutiZaring] p. 44.
(Contributed by NM, 18Aug1993.)

⊢ ∩∅ = V 

Theorem  intss1 3941 
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, 18Nov1995.)

⊢ (A ∈ B →
∩B ⊆ A) 

Theorem  ssint 3942* 
Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52
and its converse. (Contributed by NM, 14Oct1999.)

⊢ (A ⊆ ∩B ↔ ∀x ∈ B A ⊆ x) 

Theorem  ssintab 3943* 
Subclass of the intersection of a class abstraction. (Contributed by
NM, 31Jul2006.) (Proof shortened by Andrew Salmon, 9Jul2011.)

⊢ (A ⊆ ∩{x ∣ φ} ↔ ∀x(φ → A ⊆ x)) 

Theorem  ssintub 3944* 
Subclass of the least upper bound. (Contributed by NM, 8Aug2000.)

⊢ A ⊆ ∩{x ∈ B ∣ A ⊆ x} 

Theorem  ssmin 3945* 
Subclass of the minimum value of class of supersets. (Contributed by
NM, 10Aug2006.)

⊢ A ⊆ ∩{x ∣ (A ⊆ x ∧ φ)} 

Theorem  intmin 3946* 
Any member of a class is the smallest of those members that include it.
(Contributed by NM, 13Aug2002.) (Proof shortened by Andrew Salmon,
9Jul2011.)

⊢ (A ∈ B →
∩{x ∈ B ∣ A ⊆ x} =
A) 

Theorem  intss 3947 
Intersection of subclasses. (Contributed by NM, 14Oct1999.)

⊢ (A ⊆ B →
∩B ⊆ ∩A) 

Theorem  intssuni 3948 
The intersection of a nonempty set is a subclass of its union.
(Contributed by NM, 29Jul2006.)

⊢ (A ≠
∅ → ∩A ⊆ ∪A) 

Theorem  ssintrab 3949* 
Subclass of the intersection of a restricted class builder.
(Contributed by NM, 30Jan2015.)

⊢ (A ⊆ ∩{x ∈ B ∣ φ} ↔ ∀x ∈ B (φ → A ⊆ x)) 

Theorem  unissint 3950 
If the union of a class is included in its intersection, the class is
either the empty set or a singleton (uniintsn 3963). (Contributed by NM,
30Oct2010.) (Proof shortened by Andrew Salmon, 25Jul2011.)

⊢ (∪A ⊆ ∩A ↔ (A = ∅ ∨ ∪A = ∩A)) 

Theorem  intssuni2 3951 
Subclass relationship for intersection and union. (Contributed by NM,
29Jul2006.)

⊢ ((A ⊆ B ∧ A ≠ ∅) → ∩A ⊆ ∪B) 

Theorem  intminss 3952* 
Under subset ordering, the intersection of a restricted class
abstraction is less than or equal to any of its members. (Contributed
by NM, 7Sep2013.)

⊢ (x =
A → (φ ↔ ψ)) ⇒ ⊢ ((A ∈ B ∧ ψ) →
∩{x ∈ B ∣ φ}
⊆ A) 

Theorem  intmin2 3953* 
Any set is the smallest of all sets that include it. (Contributed by
NM, 20Sep2003.)

⊢ A ∈ V ⇒ ⊢ ∩{x ∣ A ⊆ x} = A 

Theorem  intmin3 3954* 
Under subset ordering, the intersection of a class abstraction is less
than or equal to any of its members. (Contributed by NM,
3Jul2005.)

⊢ (x =
A → (φ ↔ ψ))
& ⊢ ψ ⇒ ⊢ (A ∈ V →
∩{x ∣ φ}
⊆ A) 

Theorem  intmin4 3955* 
Elimination of a conjunct in a class intersection. (Contributed by NM,
31Jul2006.)

⊢ (A ⊆ ∩{x ∣ φ} → ∩{x ∣ (A ⊆ x ∧ φ)} =
∩{x ∣ φ}) 

Theorem  intab 3956* 
The intersection of a special case of a class abstraction. y may be
free in φ and
A, which can be thought of a
φ(y) and
A(y). Typically, abrexex2 (future) or
abexssex (future) can be used to
satisfy the second hypothesis. (Contributed by NM, 28Jul2006.)
(Proof shortened by Mario Carneiro, 14Nov2016.)

⊢ A ∈ V
& ⊢ {x ∣ ∃y(φ ∧ x = A)} ∈
V ⇒ ⊢ ∩{x ∣ ∀y(φ → A ∈ x)} = {x ∣ ∃y(φ ∧ x = A)} 

Theorem  int0el 3957 
The intersection of a class containing the empty set is empty.
(Contributed by NM, 24Apr2004.)

⊢ (∅ ∈ A →
∩A = ∅) 

Theorem  intun 3958 
The class intersection of the union of two classes. Theorem 78 of
[Suppes] p. 42. (Contributed by NM,
22Sep2002.)

⊢ ∩(A ∪ B) =
(∩A ∩ ∩B) 

Theorem  intpr 3959 
The intersection of a pair is the intersection of its members. Theorem
71 of [Suppes] p. 42. (Contributed by
NM, 14Oct1999.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ∩{A, B} =
(A ∩ B) 

Theorem  intprg 3960 
The intersection of a pair is the intersection of its members. Closed
form of intpr 3959. Theorem 71 of [Suppes] p. 42. (Contributed by FL,
27Apr2008.)

⊢ ((A ∈ V ∧ B ∈ W) →
∩{A, B} = (A ∩
B)) 

Theorem  intsng 3961 
Intersection of a singleton. (Contributed by Stefan O'Rear,
22Feb2015.)

⊢ (A ∈ V →
∩{A} = A) 

Theorem  intsn 3962 
The intersection of a singleton is its member. Theorem 70 of [Suppes]
p. 41. (Contributed by NM, 29Sep2002.)

⊢ A ∈ V ⇒ ⊢ ∩{A} = A 

Theorem  uniintsn 3963* 
Two ways to express "A
is a singleton." See also en1 (future), en1b (future),
card1 (future), and eusn 3796.
(Contributed by NM, 2Aug2010.)

⊢ (∪A = ∩A ↔ ∃x A = {x}) 

Theorem  uniintab 3964 
The union and the intersection of a class abstraction are equal exactly
when there is a unique satisfying value of φ(x). (Contributed
by Mario Carneiro, 24Dec2016.)

⊢ (∃!xφ ↔
∪{x ∣ φ} =
∩{x ∣ φ}) 

Theorem  intunsn 3965 
Theorem joining a singleton to an intersection. (Contributed by NM,
29Sep2002.)

⊢ B ∈ V ⇒ ⊢ ∩(A ∪ {B}) =
(∩A ∩
B) 

Theorem  rint0 3966 
Relative intersection of an empty set. (Contributed by Stefan O'Rear,
3Apr2015.)

⊢ (X = ∅ → (A
∩ ∩X) =
A) 

Theorem  elrint 3967* 
Membership in a restricted intersection. (Contributed by Stefan O'Rear,
3Apr2015.)

⊢ (X ∈ (A ∩
∩B) ↔
(X ∈
A ∧ ∀y ∈ B X ∈ y)) 

Theorem  elrint2 3968* 
Membership in a restricted intersection. (Contributed by Stefan O'Rear,
3Apr2015.)

⊢ (X ∈ A →
(X ∈
(A ∩ ∩B) ↔ ∀y ∈ B X ∈ y)) 

2.1.19 Indexed union and
intersection


Syntax  ciun 3969 
Extend class notation to include indexed union. Note: Historically
(prior to 21Oct2005), set.mm used the notation ∪x ∈ AB, with
the same union symbol as cuni 3891. 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
∪x ∈ A B 

Syntax  ciin 3970 
Extend class notation to include indexed intersection. Note:
Historically (prior to 21Oct2005), set.mm used the notation
∩x
∈ AB, with
the same intersection symbol as cint 3926. 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
∩x ∈ A B 

Definition  dfiun 3971* 
Define indexed union. Definition indexed union in [Stoll] p. 45. In
most applications, A
is independent of x (although
this is not
required by the definition), and B depends on x i.e. can be read
informally as B(x). We call x the index, A the index
set, and B the indexed
set. In most books, x ∈ A 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 x and A are in the
same distinct variable group (meaning A cannot depend on x) and
that B and x do not share a distinct variable
group (meaning
that can be thought of as B(x) i.e.
can be substituted with a
class expression containing x). An alternate definition tying
indexed union to ordinary union is dfiun2 4001. Theorem uniiun 4019 provides
a definition of ordinary union in terms of indexed union. Theorems
fniunfv 5506 and funiunfv 5507 are useful when B is a function.
(Contributed by NM, 27Jun1998.)

⊢ ∪x ∈ A B = {y ∣ ∃x ∈ A y ∈ B} 

Definition  dfiin 3972* 
Define indexed intersection. Definition of [Stoll] p. 45. See the
remarks for its sibling operation of indexed union dfiun 3971. An
alternate definition tying indexed intersection to ordinary intersection
is dfiin2 4002. Theorem intiin 4020 provides a definition of ordinary
intersection in terms of indexed intersection. (Contributed by NM,
27Jun1998.)

⊢ ∩x ∈ A B = {y ∣ ∀x ∈ A y ∈ B} 

Theorem  eliun 3973* 
Membership in indexed union. (Contributed by NM, 3Sep2003.)

⊢ (A ∈ ∪x ∈ B C ↔
∃x
∈ B
A ∈
C) 

Theorem  eliin 3974* 
Membership in indexed intersection. (Contributed by NM, 3Sep2003.)

⊢ (A ∈ V →
(A ∈
∩x ∈ B C ↔ ∀x ∈ B A ∈ C)) 

Theorem  iuncom 3975* 
Commutation of indexed unions. (Contributed by NM, 18Dec2008.)

⊢ ∪x ∈ A ∪y ∈ B C = ∪y ∈ B ∪x ∈ A C 

Theorem  iuncom4 3976 
Commutation of union with indexed union. (Contributed by Mario
Carneiro, 18Jan2014.)

⊢ ∪x ∈ A ∪B = ∪∪x ∈ A B 

Theorem  iunconst 3977* 
Indexed union of a constant class, i.e. where B does not depend on
x. (Contributed by
NM, 5Sep2004.) (Proof shortened by Andrew
Salmon, 25Jul2011.)

⊢ (A ≠
∅ → ∪x ∈ A B = B) 

Theorem  iinconst 3978* 
Indexed intersection of a constant class, i.e. where B does not
depend on x.
(Contributed by Mario Carneiro, 6Feb2015.)

⊢ (A ≠
∅ → ∩x ∈ A B = B) 

Theorem  iuniin 3979* 
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, 17Aug2004.) (Proof shortened by Andrew Salmon,
25Jul2011.)

⊢ ∪x ∈ A ∩y ∈ B C ⊆ ∩y ∈ B ∪x ∈ A C 

Theorem  iunss1 3980* 
Subclass theorem for indexed union. (Contributed by NM, 10Dec2004.)
(Proof shortened by Andrew Salmon, 25Jul2011.)

⊢ (A ⊆ B →
∪x ∈ A C ⊆ ∪x ∈ B C) 

Theorem  iinss1 3981* 
Subclass theorem for indexed union. (Contributed by NM,
24Jan2012.)

⊢ (A ⊆ B →
∩x ∈ B C ⊆ ∩x ∈ A C) 

Theorem  iuneq1 3982* 
Equality theorem for indexed union. (Contributed by NM,
27Jun1998.)

⊢ (A =
B → ∪x ∈ A C = ∪x ∈ B C) 

Theorem  iineq1 3983* 
Equality theorem for restricted existential quantifier. (Contributed by
NM, 27Jun1998.)

⊢ (A =
B → ∩x ∈ A C = ∩x ∈ B C) 

Theorem  ss2iun 3984 
Subclass theorem for indexed union. (Contributed by NM, 26Nov2003.)
(Proof shortened by Andrew Salmon, 25Jul2011.)

⊢ (∀x ∈ A B ⊆ C →
∪x ∈ A B ⊆ ∪x ∈ A C) 

Theorem  iuneq2 3985 
Equality theorem for indexed union. (Contributed by NM,
22Oct2003.)

⊢ (∀x ∈ A B = C → ∪x ∈ A B = ∪x ∈ A C) 

Theorem  iineq2 3986 
Equality theorem for indexed intersection. (Contributed by NM,
22Oct2003.) (Proof shortened by Andrew Salmon, 25Jul2011.)

⊢ (∀x ∈ A B = C → ∩x ∈ A B = ∩x ∈ A C) 

Theorem  iuneq2i 3987 
Equality inference for indexed union. (Contributed by NM,
22Oct2003.)

⊢ (x ∈ A →
B = C) ⇒ ⊢ ∪x ∈ A B = ∪x ∈ A C 

Theorem  iineq2i 3988 
Equality inference for indexed intersection. (Contributed by NM,
22Oct2003.)

⊢ (x ∈ A →
B = C) ⇒ ⊢ ∩x ∈ A B = ∩x ∈ A C 

Theorem  iineq2d 3989 
Equality deduction for indexed intersection. (Contributed by NM,
7Dec2011.)

⊢ Ⅎxφ
& ⊢ ((φ
∧ x ∈ A) →
B = C) ⇒ ⊢ (φ
→ ∩x ∈ A B = ∩x ∈ A C) 

Theorem  iuneq2dv 3990* 
Equality deduction for indexed union. (Contributed by NM,
3Aug2004.)

⊢ ((φ
∧ x ∈ A) →
B = C) ⇒ ⊢ (φ
→ ∪x ∈ A B = ∪x ∈ A C) 

Theorem  iineq2dv 3991* 
Equality deduction for indexed intersection. (Contributed by NM,
3Aug2004.)

⊢ ((φ
∧ x ∈ A) →
B = C) ⇒ ⊢ (φ
→ ∩x ∈ A B = ∩x ∈ A C) 

Theorem  iuneq1d 3992* 
Equality theorem for indexed union, deduction version. (Contributed by
Drahflow, 22Oct2015.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ ∪x ∈ A C = ∪x ∈ B C) 

Theorem  iuneq12d 3993* 
Equality deduction for indexed union, deduction version. (Contributed
by Drahflow, 22Oct2015.)

⊢ (φ
→ A = B)
& ⊢ (φ
→ C = D) ⇒ ⊢ (φ
→ ∪x ∈ A C = ∪x ∈ B D) 

Theorem  iuneq2d 3994* 
Equality deduction for indexed union. (Contributed by Drahflow,
22Oct2015.)

⊢ (φ
→ B = C) ⇒ ⊢ (φ
→ ∪x ∈ A B = ∪x ∈ A C) 

Theorem  nfiun 3995 
Boundvariable hypothesis builder for indexed union. (Contributed by
Mario Carneiro, 25Jan2014.)

⊢ F/_yA & ⊢ F/_yB ⇒ ⊢ F/_y∪x ∈ A B 

Theorem  nfiin 3996 
Boundvariable hypothesis builder for indexed intersection.
(Contributed by Mario Carneiro, 25Jan2014.)

⊢ F/_yA & ⊢ F/_yB ⇒ ⊢ F/_y∩x ∈ A B 

Theorem  nfiu1 3997 
Boundvariable hypothesis builder for indexed union. (Contributed by
NM, 12Oct2003.)

⊢ F/_x∪x ∈ A B 

Theorem  nfii1 3998 
Boundvariable hypothesis builder for indexed intersection.
(Contributed by NM, 15Oct2003.)

⊢ F/_x∩x ∈ A B 

Theorem  dfiun2g 3999* 
Alternate definition of indexed union when B is a set. Definition
15(a) of [Suppes] p. 44. (Contributed by
NM, 23Mar2006.) (Proof
shortened by Andrew Salmon, 25Jul2011.)

⊢ (∀x ∈ A B ∈ C →
∪x ∈ A B = ∪{y ∣ ∃x ∈ A y = B}) 

Theorem  dfiin2g 4000* 
Alternate definition of indexed intersection when B is a set.
(Contributed by Jeff Hankins, 27Aug2009.)

⊢ (∀x ∈ A B ∈ C →
∩x ∈ A B = ∩{y ∣ ∃x ∈ A y = B}) 