Type  Label  Description 
Statement 

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

⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵) 

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

⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ⊆ ∪ 𝐶) 

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

⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ∪
𝐴 ⊆ ∪ 𝐵 

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

⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵) 

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

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

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

⊢ (∪ 𝐴 = ∅ ↔ ∀𝑥 ∈ 𝐴 𝑥 = ∅) 

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

⊢ ∪ ∅ =
∅ 

Theorem  elssuni 3608 
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.)

⊢ (𝐴 ∈ 𝐵 → 𝐴 ⊆ ∪ 𝐵) 

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

⊢ ((∪ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐴) → ∪ 𝐴 = 𝐵) 

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

⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) 

Theorem  uniss2 3611* 
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, 22Mar2004.)

⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∪ 𝐴 ⊆ ∪ 𝐵) 

Theorem  unidif 3612* 
If the difference 𝐴 ∖ 𝐵 contains the largest members of
𝐴,
then
the union of the difference is the union of 𝐴. (Contributed by NM,
22Mar2004.)

⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ (𝐴 ∖ 𝐵)𝑥 ⊆ 𝑦 → ∪ (𝐴 ∖ 𝐵) = ∪ 𝐴) 

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

⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝑥 ⊆ 𝐴) → 𝐴 = ∪ 𝐵) 

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

⊢ (𝐴 ∈ 𝐵 → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} = 𝐴) 

2.1.19 The intersection of a class


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

class ∩ 𝐴 

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

⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦)} 

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

⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} 

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

⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩
𝐵) 

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

⊢ 𝐴 = 𝐵 ⇒ ⊢ ∩
𝐴 = ∩ 𝐵 

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

⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∩ 𝐴 = ∩
𝐵) 

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

⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥)) 

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

⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) 

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

⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)) 

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

⊢ (𝐴 ∈ ∩ 𝐵 → (𝐶 ∈ 𝐵 → 𝐴 ∈ 𝐶)) 

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

⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥∩
𝐴 

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

⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)) 

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

⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥)) 

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

⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥))) 

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

⊢ ∩ ∅ =
V 

Theorem  intss1 3630 
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.)

⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴) 

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

⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥) 

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

⊢ (𝐴 ⊆ ∩
{𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ⊆ 𝑥)) 

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

⊢ 𝐴 ⊆ ∩
{𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} 

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

⊢ 𝐴 ⊆ ∩
{𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)} 

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

⊢ (𝐴 ∈ 𝐵 → ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} = 𝐴) 

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

⊢ (𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴) 

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

⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ ∪ 𝐴) 

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

⊢ (𝐴 ⊆ ∩
{𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ⊆ 𝑥)) 

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

⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ⊆ ∪ 𝐵) 

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

⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∩
{𝑥 ∈ 𝐵 ∣ 𝜑} ⊆ 𝐴) 

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

⊢ 𝐴 ∈ V ⇒ ⊢ ∩
{𝑥 ∣ 𝐴 ⊆ 𝑥} = 𝐴 

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

⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ (𝐴 ∈ 𝑉 → ∩ {𝑥 ∣ 𝜑} ⊆ 𝐴) 

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

⊢ (𝐴 ⊆ ∩
{𝑥 ∣ 𝜑} → ∩
{𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)} = ∩ {𝑥 ∣ 𝜑}) 

Theorem  intab 3644* 
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, 28Jul2006.)
(Proof shortened by
Mario Carneiro, 14Nov2016.)

⊢ 𝐴 ∈ V & ⊢ {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} ∈ V ⇒ ⊢ ∩
{𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} 

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

⊢ (∅ ∈ 𝐴 → ∩ 𝐴 = ∅) 

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

⊢ ∩ (𝐴 ∪ 𝐵) = (∩ 𝐴 ∩ ∩ 𝐵) 

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

⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∩
{𝐴, 𝐵} = (𝐴 ∩ 𝐵) 

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

⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩
{𝐴, 𝐵} = (𝐴 ∩ 𝐵)) 

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

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

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

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

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

⊢ (∃𝑥 𝐴 = {𝑥} → ∪ 𝐴 = ∩
𝐴) 

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

⊢ (∃!𝑥𝜑 → ∪ {𝑥 ∣ 𝜑} = ∩ {𝑥 ∣ 𝜑}) 

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

⊢ 𝐵 ∈ V ⇒ ⊢ ∩
(𝐴 ∪ {𝐵}) = (∩ 𝐴
∩ 𝐵) 

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

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

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

⊢ (𝑋 ∈ (𝐴 ∩ ∩ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 𝑋 ∈ 𝑦)) 

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

⊢ (𝑋 ∈ 𝐴 → (𝑋 ∈ (𝐴 ∩ ∩ 𝐵) ↔ ∀𝑦 ∈ 𝐵 𝑋 ∈ 𝑦)) 

2.1.20 Indexed union and
intersection


Syntax  ciun 3657 
Extend class notation to include indexed union. Note: Historically
(prior to 21Oct2005), set.mm used the notation ∪ 𝑥
∈ 𝐴𝐵, with
the same union symbol as cuni 3580. 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 3658 
Extend class notation to include indexed intersection. Note:
Historically (prior to 21Oct2005), set.mm used the notation
∩ 𝑥 ∈ 𝐴𝐵, with the same intersection symbol
as cint 3615. 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  dfiun 3659* 
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 3691. Theorem uniiun 3710 provides
a definition of ordinary union in terms of indexed union. (Contributed
by NM, 27Jun1998.)

⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} 

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

⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} 

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

⊢ (𝐴 ∈ ∪
𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶) 

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

⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩
𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) 

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

⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = ∪
𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶 

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

⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝐵 = ∪
∪ 𝑥 ∈ 𝐴 𝐵 

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

⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∪
𝑥 ∈ 𝐴 𝐵 = 𝐵) 

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

⊢ (∃𝑦 𝑦 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 𝐵 = 𝐵) 

Theorem  iuniin 3667* 
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.)

⊢ ∪ 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 ⊆ ∩ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶 

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

⊢ (𝐴 ⊆ 𝐵 → ∪
𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶) 

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

⊢ (𝐴 ⊆ 𝐵 → ∩
𝑥 ∈ 𝐵 𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶) 

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

⊢ (𝐴 = 𝐵 → ∪
𝑥 ∈ 𝐴 𝐶 = ∪
𝑥 ∈ 𝐵 𝐶) 

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

⊢ (𝐴 = 𝐵 → ∩
𝑥 ∈ 𝐴 𝐶 = ∩
𝑥 ∈ 𝐵 𝐶) 

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

⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∪
𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶) 

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

⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪
𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 𝐶) 

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

⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩
𝑥 ∈ 𝐴 𝐶) 

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

⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 𝐶 

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

⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩
𝑥 ∈ 𝐴 𝐶 

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

⊢ Ⅎ𝑥𝜑
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩
𝑥 ∈ 𝐴 𝐶) 

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

⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∪
𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 𝐶) 

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

⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩
𝑥 ∈ 𝐴 𝐶) 

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

⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∪
𝑥 ∈ 𝐴 𝐶 = ∪
𝑥 ∈ 𝐵 𝐶) 

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

⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∪
𝑥 ∈ 𝐴 𝐶 = ∪
𝑥 ∈ 𝐵 𝐷) 

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

⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∪
𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 𝐶) 

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

⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵 

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

⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵 

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

⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵 

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

⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵 

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

⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 

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

⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵 

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

⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪
𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) 

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

⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) 

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

⊢ 𝐵 ∈ V ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} 

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

⊢ 𝐵 ∈ V ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} 

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

⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 ∈ 𝐶} 

Theorem  cbviun 3694* 
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.)

⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑥𝐶
& ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪
𝑦 ∈ 𝐴 𝐶 

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

⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑥𝐶
& ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩
𝑦 ∈ 𝐴 𝐶 

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

⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪
𝑦 ∈ 𝐴 𝐶 

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

⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩
𝑦 ∈ 𝐴 𝐶 

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

⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) 

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

⊢ (∃𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) 

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

⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) 