Type  Label  Description 
Statement 

Theorem  rexss 3001* 
Restricted existential quantification on a subset in terms of superset.
(Contributed by Stefan O'Rear, 3Apr2015.)

⊢ (A ⊆
B → (∃x ∈ A φ ↔ ∃x ∈ B (x ∈ A ∧ φ))) 

Theorem  ss2ab 3002 
Class abstractions in a subclass relationship. (Contributed by NM,
3Jul1994.)

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

Theorem  abss 3003* 
Class abstraction in a subclass relationship. (Contributed by NM,
16Aug2006.)

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

Theorem  ssab 3004* 
Subclass of a class abstraction. (Contributed by NM, 16Aug2006.)

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

Theorem  ssabral 3005* 
The relation for a subclass of a class abstraction is equivalent to
restricted quantification. (Contributed by NM, 6Sep2006.)

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

Theorem  ss2abi 3006 
Inference of abstraction subclass from implication. (Contributed by NM,
31Mar1995.)

⊢ (φ
→ ψ)
⇒ ⊢ {x ∣ φ} ⊆ {x ∣ ψ} 

Theorem  ss2abdv 3007* 
Deduction of abstraction subclass from implication. (Contributed by NM,
29Jul2011.)

⊢ (φ
→ (ψ → χ)) ⇒ ⊢ (φ → {x ∣ ψ} ⊆ {x ∣ χ}) 

Theorem  abssdv 3008* 
Deduction of abstraction subclass from implication. (Contributed by NM,
20Jan2006.)

⊢ (φ
→ (ψ → x ∈ A)) ⇒ ⊢ (φ → {x ∣ ψ} ⊆ A) 

Theorem  abssi 3009* 
Inference of abstraction subclass from implication. (Contributed by NM,
20Jan2006.)

⊢ (φ
→ x ∈ A) ⇒ ⊢ {x ∣ φ} ⊆ A 

Theorem  ss2rab 3010 
Restricted abstraction classes in a subclass relationship. (Contributed
by NM, 30May1999.)

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

Theorem  rabss 3011* 
Restricted class abstraction in a subclass relationship. (Contributed
by NM, 16Aug2006.)

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

Theorem  ssrab 3012* 
Subclass of a restricted class abstraction. (Contributed by NM,
16Aug2006.)

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

Theorem  ssrabdv 3013* 
Subclass of a restricted class abstraction (deduction rule).
(Contributed by NM, 31Aug2006.)

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

Theorem  rabssdv 3014* 
Subclass of a restricted class abstraction (deduction rule).
(Contributed by NM, 2Feb2015.)

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

Theorem  ss2rabdv 3015* 
Deduction of restricted abstraction subclass from implication.
(Contributed by NM, 30May2006.)

⊢ ((φ
∧ x ∈ A) →
(ψ → χ)) ⇒ ⊢ (φ → {x ∈ A ∣ ψ} ⊆ {x ∈ A ∣ χ}) 

Theorem  ss2rabi 3016 
Inference of restricted abstraction subclass from implication.
(Contributed by NM, 14Oct1999.)

⊢ (x ∈ A →
(φ → ψ)) ⇒ ⊢ {x ∈ A ∣ φ} ⊆ {x ∈ A ∣ ψ} 

Theorem  rabss2 3017* 
Subclass law for restricted abstraction. (Contributed by NM,
18Dec2004.) (Proof shortened by Andrew Salmon, 26Jun2011.)

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

Theorem  ssab2 3018* 
Subclass relation for the restriction of a class abstraction.
(Contributed by NM, 31Mar1995.)

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

Theorem  ssrab2 3019* 
Subclass relation for a restricted class. (Contributed by NM,
19Mar1997.)

⊢ {x ∈ A ∣
φ} ⊆ A 

Theorem  ssrabeq 3020* 
If the restricting class of a restricted class abstraction is a subset
of this restricted class abstraction, it is equal to this restricted
class abstraction. (Contributed by Alexander van der Vekens,
31Dec2017.)

⊢ (𝑉 ⊆ {x ∈ 𝑉 ∣ φ} ↔ 𝑉 = {x
∈ 𝑉 ∣ φ}) 

Theorem  rabssab 3021 
A restricted class is a subclass of the corresponding unrestricted class.
(Contributed by Mario Carneiro, 23Dec2016.)

⊢ {x ∈ A ∣
φ} ⊆ {x ∣ φ} 

Theorem  uniiunlem 3022* 
A subset relationship useful for converting union to indexed union using
dfiun2 or dfiun2g and intersection to indexed intersection using
dfiin2 . (Contributed by NM, 5Oct2006.) (Proof shortened by Mario
Carneiro, 26Sep2015.)

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

Theorem  dfpss2 3023 
Alternate definition of proper subclass. (Contributed by NM,
7Feb1996.)

⊢ (A ⊊
B ↔ (A ⊆ B
∧ ¬ A
= B)) 

Theorem  dfpss3 3024 
Alternate definition of proper subclass. (Contributed by NM,
7Feb1996.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ (A ⊊
B ↔ (A ⊆ B
∧ ¬ B
⊆ A)) 

Theorem  psseq1 3025 
Equality theorem for proper subclass. (Contributed by NM, 7Feb1996.)

⊢ (A =
B → (A ⊊ 𝐶 ↔ B ⊊ 𝐶)) 

Theorem  psseq2 3026 
Equality theorem for proper subclass. (Contributed by NM, 7Feb1996.)

⊢ (A =
B → (𝐶 ⊊ A ↔ 𝐶 ⊊ B)) 

Theorem  psseq1i 3027 
An equality inference for the proper subclass relationship.
(Contributed by NM, 9Jun2004.)

⊢ A =
B ⇒ ⊢ (A ⊊ 𝐶 ↔ B ⊊ 𝐶) 

Theorem  psseq2i 3028 
An equality inference for the proper subclass relationship.
(Contributed by NM, 9Jun2004.)

⊢ A =
B ⇒ ⊢ (𝐶 ⊊ A ↔ 𝐶 ⊊ B) 

Theorem  psseq12i 3029 
An equality inference for the proper subclass relationship.
(Contributed by NM, 9Jun2004.)

⊢ A =
B & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (A ⊊ 𝐶 ↔ B ⊊ 𝐷) 

Theorem  psseq1d 3030 
An equality deduction for the proper subclass relationship.
(Contributed by NM, 9Jun2004.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ → (A ⊊ 𝐶 ↔ B ⊊ 𝐶)) 

Theorem  psseq2d 3031 
An equality deduction for the proper subclass relationship.
(Contributed by NM, 9Jun2004.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ → (𝐶 ⊊ A ↔ 𝐶 ⊊ B)) 

Theorem  psseq12d 3032 
An equality deduction for the proper subclass relationship.
(Contributed by NM, 9Jun2004.)

⊢ (φ
→ A = B)
& ⊢ (φ
→ 𝐶 = 𝐷)
⇒ ⊢ (φ → (A ⊊ 𝐶 ↔ B ⊊ 𝐷)) 

Theorem  pssss 3033 
A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23.
(Contributed by NM, 7Feb1996.)

⊢ (A ⊊
B → A ⊆ B) 

Theorem  pssne 3034 
Two classes in a proper subclass relationship are not equal. (Contributed
by NM, 16Feb2015.)

⊢ (A ⊊
B → A ≠ B) 

Theorem  pssssd 3035 
Deduce subclass from proper subclass. (Contributed by NM,
29Feb1996.)

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

Theorem  pssned 3036 
Proper subclasses are unequal. Deduction form of pssne 3034.
(Contributed by David Moews, 1May2017.)

⊢ (φ
→ A ⊊ B) ⇒ ⊢ (φ → A ≠ B) 

Theorem  sspssr 3037 
Subclass in terms of proper subclass. (Contributed by Jim Kingdon,
16Jul2018.)

⊢ ((A
⊊ B
∨ A = B) → A
⊆ B) 

Theorem  pssirr 3038 
Proper subclass is irreflexive. Theorem 7 of [Suppes] p. 23.
(Contributed by NM, 7Feb1996.)

⊢ ¬ A
⊊ A 

Theorem  pssn2lp 3039 
Proper subclass has no 2cycle loops. Compare Theorem 8 of [Suppes]
p. 23. (Contributed by NM, 7Feb1996.) (Proof shortened by Andrew
Salmon, 26Jun2011.)

⊢ ¬ (A
⊊ B ∧ B ⊊
A) 

Theorem  sspsstrir 3040 
Two ways of stating trichotomy with respect to inclusion. (Contributed by
Jim Kingdon, 16Jul2018.)

⊢ ((A
⊊ B
∨ A = B ∨ B ⊊ A)
→ (A ⊆ B ∨ B ⊆ A)) 

Theorem  ssnpss 3041 
Partial trichotomy law for subclasses. (Contributed by NM, 16May1996.)
(Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ (A ⊆
B → ¬ B ⊊ A) 

Theorem  sspssn 3042 
Like pssn2lp 3039 but for subset and proper subset.
(Contributed by Jim
Kingdon, 17Jul2018.)

⊢ ¬ (A
⊆ B ∧ B ⊊
A) 

Theorem  psstr 3043 
Transitive law for proper subclass. Theorem 9 of [Suppes] p. 23.
(Contributed by NM, 7Feb1996.)

⊢ ((A
⊊ B ∧ B ⊊
𝐶) → A ⊊ 𝐶) 

Theorem  sspsstr 3044 
Transitive law for subclass and proper subclass. (Contributed by NM,
3Apr1996.)

⊢ ((A ⊆
B ∧
B ⊊ 𝐶) → A ⊊ 𝐶) 

Theorem  psssstr 3045 
Transitive law for subclass and proper subclass. (Contributed by NM,
3Apr1996.)

⊢ ((A
⊊ B ∧ B ⊆
𝐶) → A ⊊ 𝐶) 

Theorem  psstrd 3046 
Proper subclass inclusion is transitive. Deduction form of psstr 3043.
(Contributed by David Moews, 1May2017.)

⊢ (φ
→ A ⊊ B)
& ⊢ (φ
→ B ⊊ 𝐶) ⇒ ⊢ (φ → A ⊊ 𝐶) 

Theorem  sspsstrd 3047 
Transitivity involving subclass and proper subclass inclusion.
Deduction form of sspsstr 3044. (Contributed by David Moews,
1May2017.)

⊢ (φ
→ A ⊆ B)
& ⊢ (φ
→ B ⊊ 𝐶) ⇒ ⊢ (φ → A ⊊ 𝐶) 

Theorem  psssstrd 3048 
Transitivity involving subclass and proper subclass inclusion.
Deduction form of psssstr 3045. (Contributed by David Moews,
1May2017.)

⊢ (φ
→ A ⊊ B)
& ⊢ (φ
→ B ⊆ 𝐶) ⇒ ⊢ (φ → A ⊊ 𝐶) 

2.1.13 The difference, union, and intersection
of two classes


2.1.13.1 The difference of two
classes


Theorem  difeq1 3049 
Equality theorem for class difference. (Contributed by NM,
10Feb1997.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ (A =
B → (A ∖ 𝐶) = (B
∖ 𝐶)) 

Theorem  difeq2 3050 
Equality theorem for class difference. (Contributed by NM,
10Feb1997.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ (A =
B → (𝐶 ∖ A) = (𝐶 ∖ B)) 

Theorem  difeq12 3051 
Equality theorem for class difference. (Contributed by FL,
31Aug2009.)

⊢ ((A =
B ∧ 𝐶 = 𝐷) → (A ∖ 𝐶) = (B
∖ 𝐷)) 

Theorem  difeq1i 3052 
Inference adding difference to the right in a class equality.
(Contributed by NM, 15Nov2002.)

⊢ A =
B ⇒ ⊢ (A ∖ 𝐶) = (B
∖ 𝐶) 

Theorem  difeq2i 3053 
Inference adding difference to the left in a class equality.
(Contributed by NM, 15Nov2002.)

⊢ A =
B ⇒ ⊢ (𝐶 ∖ A) = (𝐶 ∖ B) 

Theorem  difeq12i 3054 
Equality inference for class difference. (Contributed by NM,
29Aug2004.)

⊢ A =
B & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (A ∖ 𝐶) = (B
∖ 𝐷) 

Theorem  difeq1d 3055 
Deduction adding difference to the right in a class equality.
(Contributed by NM, 15Nov2002.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ → (A ∖ 𝐶) = (B
∖ 𝐶)) 

Theorem  difeq2d 3056 
Deduction adding difference to the left in a class equality.
(Contributed by NM, 15Nov2002.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ → (𝐶 ∖ A) = (𝐶 ∖ B)) 

Theorem  difeq12d 3057 
Equality deduction for class difference. (Contributed by FL,
29May2014.)

⊢ (φ
→ A = B)
& ⊢ (φ
→ 𝐶 = 𝐷)
⇒ ⊢ (φ → (A ∖ 𝐶) = (B
∖ 𝐷)) 

Theorem  difeqri 3058* 
Inference from membership to difference. (Contributed by NM,
17May1998.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ ((x ∈ A ∧ ¬ x ∈ B) ↔
x ∈
𝐶) ⇒ ⊢ (A ∖ B) =
𝐶 

Theorem  nfdif 3059 
Boundvariable hypothesis builder for class difference. (Contributed by
NM, 3Dec2003.) (Revised by Mario Carneiro, 13Oct2016.)

⊢ ℲxA & ⊢
ℲxB ⇒ ⊢ Ⅎx(A ∖
B) 

Theorem  eldifi 3060 
Implication of membership in a class difference. (Contributed by NM,
29Apr1994.)

⊢ (A ∈ (B ∖
𝐶) → A ∈ B) 

Theorem  eldifn 3061 
Implication of membership in a class difference. (Contributed by NM,
3May1994.)

⊢ (A ∈ (B ∖
𝐶) → ¬ A ∈ 𝐶) 

Theorem  elndif 3062 
A set does not belong to a class excluding it. (Contributed by NM,
27Jun1994.)

⊢ (A ∈ B →
¬ A ∈ (𝐶 ∖ B)) 

Theorem  difdif 3063 
Double class difference. Exercise 11 of [TakeutiZaring] p. 22.
(Contributed by NM, 17May1998.)

⊢ (A ∖
(B ∖ A)) = A 

Theorem  difss 3064 
Subclass relationship for class difference. Exercise 14 of
[TakeutiZaring] p. 22.
(Contributed by NM, 29Apr1994.)

⊢ (A ∖
B) ⊆ A 

Theorem  difssd 3065 
A difference of two classes is contained in the minuend. Deduction form
of difss 3064. (Contributed by David Moews, 1May2017.)

⊢ (φ
→ (A ∖ B) ⊆ A) 

Theorem  difss2 3066 
If a class is contained in a difference, it is contained in the minuend.
(Contributed by David Moews, 1May2017.)

⊢ (A ⊆
(B ∖ 𝐶) → A ⊆ B) 

Theorem  difss2d 3067 
If a class is contained in a difference, it is contained in the
minuend. Deduction form of difss2 3066. (Contributed by David Moews,
1May2017.)

⊢ (φ
→ A ⊆ (B ∖ 𝐶)) ⇒ ⊢ (φ → A ⊆ B) 

Theorem  ssdifss 3068 
Preservation of a subclass relationship by class difference. (Contributed
by NM, 15Feb2007.)

⊢ (A ⊆
B → (A ∖ 𝐶) ⊆ B) 

Theorem  ddifnel 3069* 
Double complement under universal class. The hypothesis is one way of
expressing the idea that membership in A is decidable. Exercise
4.10(s) of [Mendelson] p. 231, but
with an additional hypothesis. For a
version without a hypothesis, but which only states that A is a
subset of V ∖ (V ∖ A), see ddifss 3169. (Contributed by Jim
Kingdon, 21Jul2018.)

⊢ (¬ x
∈ (V ∖ A) → x
∈ A) ⇒ ⊢ (V ∖ (V ∖ A)) = A 

Theorem  ssconb 3070 
Contraposition law for subsets. (Contributed by NM, 22Mar1998.)

⊢ ((A ⊆
𝐶 ∧ B ⊆
𝐶) → (A ⊆ (𝐶 ∖ B) ↔ B
⊆ (𝐶 ∖
A))) 

Theorem  sscon 3071 
Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22.
(Contributed by NM, 22Mar1998.)

⊢ (A ⊆
B → (𝐶 ∖ B) ⊆ (𝐶 ∖ A)) 

Theorem  ssdif 3072 
Difference law for subsets. (Contributed by NM, 28May1998.)

⊢ (A ⊆
B → (A ∖ 𝐶) ⊆ (B ∖ 𝐶)) 

Theorem  ssdifd 3073 
If A is contained
in B, then (A ∖ 𝐶) is contained in
(B ∖ 𝐶). Deduction form of ssdif 3072. (Contributed by David
Moews, 1May2017.)

⊢ (φ
→ A ⊆ B) ⇒ ⊢ (φ → (A ∖ 𝐶) ⊆ (B ∖ 𝐶)) 

Theorem  sscond 3074 
If A is contained
in B, then (𝐶 ∖
B) is contained in
(𝐶
∖ A). Deduction form of sscon 3071. (Contributed by David
Moews, 1May2017.)

⊢ (φ
→ A ⊆ B) ⇒ ⊢ (φ → (𝐶 ∖ B) ⊆ (𝐶 ∖ A)) 

Theorem  ssdifssd 3075 
If A is contained
in B, then (A ∖ 𝐶) is also contained in
B.
Deduction form of ssdifss 3068. (Contributed by David Moews,
1May2017.)

⊢ (φ
→ A ⊆ B) ⇒ ⊢ (φ → (A ∖ 𝐶) ⊆ B) 

Theorem  ssdif2d 3076 
If A is contained
in B and 𝐶 is
contained in 𝐷, then
(A ∖ 𝐷) is contained in (B ∖ 𝐶). Deduction form.
(Contributed by David Moews, 1May2017.)

⊢ (φ
→ A ⊆ B)
& ⊢ (φ
→ 𝐶 ⊆ 𝐷)
⇒ ⊢ (φ → (A ∖ 𝐷) ⊆ (B ∖ 𝐶)) 

Theorem  raldifb 3077 
Restricted universal quantification on a class difference in terms of an
implication. (Contributed by Alexander van der Vekens, 3Jan2018.)

⊢ (∀x ∈ A (x ∉
B → φ) ↔ ∀x ∈ (A ∖
B)φ) 

2.1.13.2 The union of two classes


Theorem  elun 3078 
Expansion of membership in class union. Theorem 12 of [Suppes] p. 25.
(Contributed by NM, 7Aug1994.)

⊢ (A ∈ (B ∪
𝐶) ↔ (A ∈ B ∨ A ∈ 𝐶)) 

Theorem  uneqri 3079* 
Inference from membership to union. (Contributed by NM, 5Aug1993.)

⊢ ((x ∈ A ∨ x ∈ B) ↔
x ∈
𝐶) ⇒ ⊢ (A ∪ B) =
𝐶 

Theorem  unidm 3080 
Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27.
(Contributed by NM, 5Aug1993.)

⊢ (A ∪
A) = A 

Theorem  uncom 3081 
Commutative law for union of classes. Exercise 6 of [TakeutiZaring]
p. 17. (Contributed by NM, 25Jun1998.) (Proof shortened by Andrew
Salmon, 26Jun2011.)

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

Theorem  equncom 3082 
If a class equals the union of two other classes, then it equals the
union of those two classes commuted. (Contributed by Alan Sare,
18Feb2012.)

⊢ (A =
(B ∪ 𝐶) ↔ A = (𝐶 ∪ B)) 

Theorem  equncomi 3083 
Inference form of equncom 3082. (Contributed by Alan Sare,
18Feb2012.)

⊢ A =
(B ∪ 𝐶) ⇒ ⊢ A = (𝐶 ∪ B) 

Theorem  uneq1 3084 
Equality theorem for union of two classes. (Contributed by NM,
5Aug1993.)

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

Theorem  uneq2 3085 
Equality theorem for the union of two classes. (Contributed by NM,
5Aug1993.)

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

Theorem  uneq12 3086 
Equality theorem for union of two classes. (Contributed by NM,
29Mar1998.)

⊢ ((A =
B ∧ 𝐶 = 𝐷) → (A ∪ 𝐶) = (B
∪ 𝐷)) 

Theorem  uneq1i 3087 
Inference adding union to the right in a class equality. (Contributed
by NM, 30Aug1993.)

⊢ A =
B ⇒ ⊢ (A ∪ 𝐶) = (B
∪ 𝐶) 

Theorem  uneq2i 3088 
Inference adding union to the left in a class equality. (Contributed by
NM, 30Aug1993.)

⊢ A =
B ⇒ ⊢ (𝐶 ∪ A) = (𝐶 ∪ B) 

Theorem  uneq12i 3089 
Equality inference for union of two classes. (Contributed by NM,
12Aug2004.) (Proof shortened by Eric Schmidt, 26Jan2007.)

⊢ A =
B & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (A ∪ 𝐶) = (B
∪ 𝐷) 

Theorem  uneq1d 3090 
Deduction adding union to the right in a class equality. (Contributed
by NM, 29Mar1998.)

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

Theorem  uneq2d 3091 
Deduction adding union to the left in a class equality. (Contributed by
NM, 29Mar1998.)

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

Theorem  uneq12d 3092 
Equality deduction for union of two classes. (Contributed by NM,
29Sep2004.) (Proof shortened by Andrew Salmon, 26Jun2011.)

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

Theorem  nfun 3093 
Boundvariable hypothesis builder for the union of classes.
(Contributed by NM, 15Sep2003.) (Revised by Mario Carneiro,
14Oct2016.)

⊢ ℲxA & ⊢
ℲxB ⇒ ⊢ Ⅎx(A ∪
B) 

Theorem  unass 3094 
Associative law for union of classes. Exercise 8 of [TakeutiZaring]
p. 17. (Contributed by NM, 3May1994.) (Proof shortened by Andrew
Salmon, 26Jun2011.)

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

Theorem  un12 3095 
A rearrangement of union. (Contributed by NM, 12Aug2004.)

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

Theorem  un23 3096 
A rearrangement of union. (Contributed by NM, 12Aug2004.) (Proof
shortened by Andrew Salmon, 26Jun2011.)

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

Theorem  un4 3097 
A rearrangement of the union of 4 classes. (Contributed by NM,
12Aug2004.)

⊢ ((A ∪
B) ∪ (𝐶 ∪ 𝐷)) = ((A ∪ 𝐶) ∪ (B ∪ 𝐷)) 

Theorem  unundi 3098 
Union distributes over itself. (Contributed by NM, 17Aug2004.)

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

Theorem  unundir 3099 
Union distributes over itself. (Contributed by NM, 17Aug2004.)

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

Theorem  ssun1 3100 
Subclass relationship for union of classes. Theorem 25 of [Suppes]
p. 27. (Contributed by NM, 5Aug1993.)

⊢ A ⊆
(A ∪ B) 