Type  Label  Description 
Statement 

Theorem  ssint 3601* 
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 3602* 
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 3603* 
Subclass of the least upper bound. (Contributed by NM, 8Aug2000.)

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

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

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

Theorem  intmin 3605* 
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 3606 
Intersection of subclasses. (Contributed by NM, 14Oct1999.)

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

Theorem  intssunim 3607* 
The intersection of an inhabited set is a subclass of its union.
(Contributed by NM, 29Jul2006.)

⊢ (∃x x ∈ A →
∩ A ⊆
∪ A) 

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

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

Theorem  intssuni2m 3609* 
Subclass relationship for intersection and union. (Contributed by Jim
Kingdon, 14Aug2018.)

⊢ ((A ⊆
B ∧ ∃x x ∈ A) → ∩ A ⊆ ∪ B) 

Theorem  intminss 3610* 
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 3611* 
Any set is the smallest of all sets that include it. (Contributed by
NM, 20Sep2003.)

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

Theorem  intmin3 3612* 
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 ∈ 𝑉 → ∩ {x ∣ φ} ⊆ A) 

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

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

Theorem  intab 3614* 
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). (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 3615 
The intersection of a class containing the empty set is empty.
(Contributed by NM, 24Apr2004.)

⊢ (∅ ∈
A → ∩
A = ∅) 

Theorem  intun 3616 
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 3617 
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 3618 
The intersection of a pair is the intersection of its members. Closed
form of intpr 3617. Theorem 71 of [Suppes] p. 42. (Contributed by FL,
27Apr2008.)

⊢ ((A ∈ 𝑉 ∧
B ∈
𝑊) → ∩ {A, B} = (A ∩
B)) 

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

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

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

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

Theorem  uniintsnr 3621* 
The union and intersection of a singleton are equal. See also eusn 3414.
(Contributed by Jim Kingdon, 14Aug2018.)

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

Theorem  uniintabim 3622 
The union and the intersection of a class abstraction are equal if there
is a unique satisfying value of φ(x). (Contributed by Jim
Kingdon, 14Aug2018.)

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

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

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

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

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

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

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

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

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

2.1.20 Indexed union and
intersection


Syntax  ciun 3627 
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 3550. 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 3628 
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 3585. 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 3629* 
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 3661. Theorem uniiun 3680 provides
a definition of ordinary union in terms of indexed union. (Contributed
by NM, 27Jun1998.)

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

Definition  dfiin 3630* 
Define indexed intersection. Definition of [Stoll] p. 45. See the
remarks for its sibling operation of indexed union dfiun 3629. An
alternate definition tying indexed intersection to ordinary intersection
is dfiin2 3662. Theorem intiin 3681 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 3631* 
Membership in indexed union. (Contributed by NM, 3Sep2003.)

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

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

⊢ (A ∈ 𝑉 → (A ∈ ∩ x ∈ B 𝐶 ↔ ∀x ∈ B A ∈ 𝐶)) 

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

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

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

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

Theorem  iunconstm 3635* 
Indexed union of a constant class, i.e. where B does not depend on
x.
(Contributed by Jim Kingdon, 15Aug2018.)

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

Theorem  iinconstm 3636* 
Indexed intersection of a constant class, i.e. where B does not
depend on x.
(Contributed by Jim Kingdon, 19Dec2018.)

⊢ (∃y y ∈ A →
∩ x
∈ A
B = B) 

Theorem  iuniin 3637* 
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 𝐶 ⊆ ∩ y ∈ B ∪ x ∈ A 𝐶 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ (φ
→ A = B)
& ⊢ (φ
→ 𝐶 = 𝐷)
⇒ ⊢ (φ → ∪
x ∈
A 𝐶 = ∪
x ∈
B 𝐷) 

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

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

Theorem  nfiunxy 3653* 
Boundvariable hypothesis builder for indexed union. (Contributed by
Mario Carneiro, 25Jan2014.)

⊢ ℲyA & ⊢
ℲyB ⇒ ⊢ Ⅎy∪ x ∈ A B 

Theorem  nfiinxy 3654* 
Boundvariable hypothesis builder for indexed intersection.
(Contributed by Mario Carneiro, 25Jan2014.)

⊢ ℲyA & ⊢
ℲyB ⇒ ⊢ Ⅎy∩ x ∈ A B 

Theorem  nfiunya 3655* 
Boundvariable hypothesis builder for indexed union. (Contributed by
Mario Carneiro, 25Jan2014.)

⊢ ℲyA & ⊢
ℲyB ⇒ ⊢ Ⅎy∪ x ∈ A B 

Theorem  nfiinya 3656* 
Boundvariable hypothesis builder for indexed intersection.
(Contributed by Mario Carneiro, 25Jan2014.)

⊢ ℲyA & ⊢
ℲyB ⇒ ⊢ Ⅎy∩ x ∈ A B 

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

⊢ Ⅎx∪ x ∈ A B 

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

⊢ Ⅎx∩ x ∈ A B 

Theorem  dfiun2g 3659* 
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 ∈ 𝐶 → ∪
x ∈
A B =
∪ {y ∣
∃x
∈ A
y = B}) 

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

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

Theorem  dfiun2 3661* 
Alternate definition of indexed union when B is a set. Definition
15(a) of [Suppes] p. 44. (Contributed by
NM, 27Jun1998.) (Revised by
David Abernethy, 19Jun2012.)

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

Theorem  dfiin2 3662* 
Alternate definition of indexed intersection when B is a set.
Definition 15(b) of [Suppes] p. 44.
(Contributed by NM, 28Jun1998.)
(Proof shortened by Andrew Salmon, 25Jul2011.)

⊢ B ∈ V ⇒ ⊢ ∩ x ∈ A B = ∩ {y ∣ ∃x ∈ A y = B} 

Theorem  dfiunv2 3663* 
Define double indexed union. (Contributed by FL, 6Nov2013.)

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

Theorem  cbviun 3664* 
Rule used to change the bound variables in an indexed union, with the
substitution specified implicitly by the hypothesis. (Contributed by
NM, 26Mar2006.) (Revised by Andrew Salmon, 25Jul2011.)

⊢ ℲyB & ⊢
Ⅎx𝐶
& ⊢ (x =
y → B = 𝐶) ⇒ ⊢ ∪ x ∈ A B = ∪ y ∈ A 𝐶 

Theorem  cbviin 3665* 
Change bound variables in an indexed intersection. (Contributed by Jeff
Hankins, 26Aug2009.) (Revised by Mario Carneiro, 14Oct2016.)

⊢ ℲyB & ⊢
Ⅎx𝐶
& ⊢ (x =
y → B = 𝐶) ⇒ ⊢ ∩ x ∈ A B = ∩ y ∈ A 𝐶 

Theorem  cbviunv 3666* 
Rule used to change the bound variables in an indexed union, with the
substitution specified implicitly by the hypothesis. (Contributed by
NM, 15Sep2003.)

⊢ (x =
y → B = 𝐶) ⇒ ⊢ ∪ x ∈ A B = ∪ y ∈ A 𝐶 

Theorem  cbviinv 3667* 
Change bound variables in an indexed intersection. (Contributed by Jeff
Hankins, 26Aug2009.)

⊢ (x =
y → B = 𝐶) ⇒ ⊢ ∩ x ∈ A B = ∩ y ∈ A 𝐶 

Theorem  iunss 3668* 
Subset theorem for an indexed union. (Contributed by NM, 13Sep2003.)
(Proof shortened by Andrew Salmon, 25Jul2011.)

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

Theorem  ssiun 3669* 
Subset implication for an indexed union. (Contributed by NM,
3Sep2003.) (Proof shortened by Andrew Salmon, 25Jul2011.)

⊢ (∃x ∈ A 𝐶 ⊆ B → 𝐶 ⊆ ∪ x ∈ A B) 

Theorem  ssiun2 3670 
Identity law for subset of an indexed union. (Contributed by NM,
12Oct2003.) (Proof shortened by Andrew Salmon, 25Jul2011.)

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

Theorem  ssiun2s 3671* 
Subset relationship for an indexed union. (Contributed by NM,
26Oct2003.)

⊢ (x = 𝐶 → B = 𝐷) ⇒ ⊢ (𝐶 ∈
A → 𝐷 ⊆ ∪ x ∈ A B) 

Theorem  iunss2 3672* 
A subclass condition on the members of two indexed classes 𝐶(x)
and 𝐷(y) that implies a subclass relation on their
indexed
unions. Generalization of Proposition 8.6 of [TakeutiZaring] p. 59.
Compare uniss2 3581. (Contributed by NM, 9Dec2004.)

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

Theorem  iunab 3673* 
The indexed union of a class abstraction. (Contributed by NM,
27Dec2004.)

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

Theorem  iunrab 3674* 
The indexed union of a restricted class abstraction. (Contributed by
NM, 3Jan2004.) (Proof shortened by Mario Carneiro, 14Nov2016.)

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

Theorem  iunxdif2 3675* 
Indexed union with a class difference as its index. (Contributed by NM,
10Dec2004.)

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

Theorem  ssiinf 3676 
Subset theorem for an indexed intersection. (Contributed by FL,
15Oct2012.) (Proof shortened by Mario Carneiro, 14Oct2016.)

⊢ Ⅎx𝐶 ⇒ ⊢ (𝐶 ⊆ ∩ x ∈ A B ↔ ∀x ∈ A 𝐶 ⊆ B) 

Theorem  ssiin 3677* 
Subset theorem for an indexed intersection. (Contributed by NM,
15Oct2003.)

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

Theorem  iinss 3678* 
Subset implication for an indexed intersection. (Contributed by NM,
15Oct2003.) (Proof shortened by Andrew Salmon, 25Jul2011.)

⊢ (∃x ∈ A B ⊆
𝐶 → ∩ x ∈ A B ⊆ 𝐶) 

Theorem  iinss2 3679 
An indexed intersection is included in any of its members. (Contributed
by FL, 15Oct2012.)

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

Theorem  uniiun 3680* 
Class union in terms of indexed union. Definition in [Stoll] p. 43.
(Contributed by NM, 28Jun1998.)

⊢ ∪ A = ∪ x ∈ A x 

Theorem  intiin 3681* 
Class intersection in terms of indexed intersection. Definition in
[Stoll] p. 44. (Contributed by NM,
28Jun1998.)

⊢ ∩ A = ∩ x ∈ A x 

Theorem  iunid 3682* 
An indexed union of singletons recovers the index set. (Contributed by
NM, 6Sep2005.)

⊢ ∪ x ∈ A {x} =
A 

Theorem  iun0 3683 
An indexed union of the empty set is empty. (Contributed by NM,
26Mar2003.) (Proof shortened by Andrew Salmon, 25Jul2011.)

⊢ ∪ x ∈ A ∅ = ∅ 

Theorem  0iun 3684 
An empty indexed union is empty. (Contributed by NM, 4Dec2004.)
(Proof shortened by Andrew Salmon, 25Jul2011.)

⊢ ∪ x ∈ ∅
A = ∅ 

Theorem  0iin 3685 
An empty indexed intersection is the universal class. (Contributed by
NM, 20Oct2005.)

⊢ ∩ x ∈ ∅
A = V 

Theorem  viin 3686* 
Indexed intersection with a universal index class. (Contributed by NM,
11Sep2008.)

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

Theorem  iunn0m 3687* 
There is an inhabited class in an indexed collection B(x) iff
the
indexed union of them is inhabited. (Contributed by Jim Kingdon,
16Aug2018.)

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

Theorem  iinab 3688* 
Indexed intersection of a class builder. (Contributed by NM,
6Dec2011.)

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

Theorem  iinrabm 3689* 
Indexed intersection of a restricted class builder. (Contributed by Jim
Kingdon, 16Aug2018.)

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

Theorem  iunin2 3690* 
Indexed union of intersection. Generalization of half of theorem
"Distributive laws" in [Enderton] p. 30. Use uniiun 3680 to recover
Enderton's theorem. (Contributed by NM, 26Mar2004.)

⊢ ∪ x ∈ A (B ∩
𝐶) = (B ∩ ∪
x ∈
A 𝐶) 

Theorem  iunin1 3691* 
Indexed union of intersection. Generalization of half of theorem
"Distributive laws" in [Enderton] p. 30. Use uniiun 3680 to recover
Enderton's theorem. (Contributed by Mario Carneiro, 30Aug2015.)

⊢ ∪ x ∈ A (𝐶 ∩ B) = (∪ x ∈ A 𝐶 ∩ B) 

Theorem  iundif2ss 3692* 
Indexed union of class difference. Compare to theorem "De Morgan's
laws" in [Enderton] p. 31.
(Contributed by Jim Kingdon,
17Aug2018.)

⊢ ∪ x ∈ A (B ∖
𝐶) ⊆ (B ∖ ∩
x ∈
A 𝐶) 

Theorem  2iunin 3693* 
Rearrange indexed unions over intersection. (Contributed by NM,
18Dec2008.)

⊢ ∪ x ∈ A ∪ y ∈ B (𝐶 ∩ 𝐷) = (∪
x ∈
A 𝐶 ∩ ∪
y ∈
B 𝐷) 

Theorem  iindif2m 3694* 
Indexed intersection of class difference. Compare to Theorem "De
Morgan's laws" in [Enderton] p.
31. (Contributed by Jim Kingdon,
17Aug2018.)

⊢ (∃x x ∈ A →
∩ x
∈ A
(B ∖ 𝐶) = (B
∖ ∪ x ∈ A 𝐶)) 

Theorem  iinin2m 3695* 
Indexed intersection of intersection. Compare to Theorem "Distributive
laws" in [Enderton] p. 30.
(Contributed by Jim Kingdon,
17Aug2018.)

⊢ (∃x x ∈ A →
∩ x
∈ A
(B ∩ 𝐶) = (B
∩ ∩ x ∈ A 𝐶)) 

Theorem  iinin1m 3696* 
Indexed intersection of intersection. Compare to Theorem "Distributive
laws" in [Enderton] p. 30.
(Contributed by Jim Kingdon,
17Aug2018.)

⊢ (∃x x ∈ A →
∩ x
∈ A
(𝐶 ∩ B) = (∩ x ∈ A 𝐶 ∩ B)) 

Theorem  elriin 3697* 
Elementhood in a relative intersection. (Contributed by Mario Carneiro,
30Dec2016.)

⊢ (B ∈ (A ∩
∩ x
∈ 𝑋 𝑆) ↔ (B ∈ A ∧ ∀x ∈ 𝑋 B
∈ 𝑆)) 

Theorem  riin0 3698* 
Relative intersection of an empty family. (Contributed by Stefan
O'Rear, 3Apr2015.)

⊢ (𝑋 = ∅ → (A ∩ ∩
x ∈
𝑋 𝑆) = A) 

Theorem  riinm 3699* 
Relative intersection of an inhabited family. (Contributed by Jim
Kingdon, 19Aug2018.)

⊢ ((∀x ∈ 𝑋 𝑆 ⊆ A ∧ ∃x x ∈ 𝑋) → (A ∩ ∩
x ∈
𝑋 𝑆) = ∩
x ∈
𝑋 𝑆) 

Theorem  iinxsng 3700* 
A singleton index picks out an instance of an indexed intersection's
argument. (Contributed by NM, 15Jan2012.) (Proof shortened by Mario
Carneiro, 17Nov2016.)

⊢ (x =
A → B = 𝐶) ⇒ ⊢ (A ∈ 𝑉 → ∩ x ∈ {A}B = 𝐶) 