Type  Label  Description 
Statement 

Theorem  notab 3201 
A class builder defined by a negation. (Contributed by FL,
18Sep2010.)

⊢ {x ∣
¬ φ} = (V ∖ {x ∣ φ}) 

Theorem  unrab 3202 
Union of two restricted class abstractions. (Contributed by NM,
25Mar2004.)

⊢ ({x ∈ A ∣
φ} ∪ {x ∈ A ∣ ψ}) = {x
∈ A
∣ (φ
∨ ψ)} 

Theorem  inrab 3203 
Intersection of two restricted class abstractions. (Contributed by NM,
1Sep2006.)

⊢ ({x ∈ A ∣
φ} ∩ {x ∈ A ∣ ψ}) = {x
∈ A
∣ (φ ∧ ψ)} 

Theorem  inrab2 3204* 
Intersection with a restricted class abstraction. (Contributed by NM,
19Nov2007.)

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

Theorem  difrab 3205 
Difference of two restricted class abstractions. (Contributed by NM,
23Oct2004.)

⊢ ({x ∈ A ∣
φ} ∖ {x ∈ A ∣ ψ}) = {x
∈ A
∣ (φ ∧ ¬ ψ)} 

Theorem  dfrab2 3206* 
Alternate definition of restricted class abstraction. (Contributed by
NM, 20Sep2003.)

⊢ {x ∈ A ∣
φ} = ({x ∣ φ} ∩ A) 

Theorem  dfrab3 3207* 
Alternate definition of restricted class abstraction. (Contributed by
Mario Carneiro, 8Sep2013.)

⊢ {x ∈ A ∣
φ} = (A ∩ {x
∣ φ}) 

Theorem  notrab 3208* 
Complementation of restricted class abstractions. (Contributed by Mario
Carneiro, 3Sep2015.)

⊢ (A ∖
{x ∈
A ∣ φ}) = {x
∈ A
∣ ¬ φ} 

Theorem  dfrab3ss 3209* 
Restricted class abstraction with a common superset. (Contributed by
Stefan O'Rear, 12Sep2015.) (Proof shortened by Mario Carneiro,
8Nov2015.)

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

Theorem  rabun2 3210 
Abstraction restricted to a union. (Contributed by Stefan O'Rear,
5Feb2015.)

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

2.1.13.6 Restricted uniqueness with difference,
union, and intersection


Theorem  reuss2 3211* 
Transfer uniqueness to a smaller subclass. (Contributed by NM,
20Oct2005.)

⊢ (((A
⊆ B ∧ ∀x ∈ A (φ →
ψ)) ∧
(∃x
∈ A
φ ∧
∃!x
∈ B
ψ)) → ∃!x ∈ A φ) 

Theorem  reuss 3212* 
Transfer uniqueness to a smaller subclass. (Contributed by NM,
21Aug1999.)

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

Theorem  reuun1 3213* 
Transfer uniqueness to a smaller class. (Contributed by NM,
21Oct2005.)

⊢ ((∃x ∈ A φ ∧ ∃!x ∈ (A ∪ B)(φ ∨ ψ))
→ ∃!x ∈ A φ) 

Theorem  reuun2 3214* 
Transfer uniqueness to a smaller or larger class. (Contributed by NM,
21Oct2005.)

⊢ (¬ ∃x ∈ B φ → (∃!x ∈ (A ∪
B)φ ↔ ∃!x ∈ A φ)) 

Theorem  reupick 3215* 
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
NM, 21Aug1999.)

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

Theorem  reupick3 3216* 
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
Mario Carneiro, 19Nov2016.)

⊢ ((∃!x ∈ A φ ∧ ∃x ∈ A (φ ∧ ψ) ∧ x ∈ A) →
(φ → ψ)) 

Theorem  reupick2 3217* 
Restricted uniqueness "picks" a member of a subclass. (Contributed
by
Mario Carneiro, 15Dec2013.) (Proof shortened by Mario Carneiro,
19Nov2016.)

⊢ (((∀x ∈ A (ψ → φ) ∧ ∃x ∈ A ψ ∧ ∃!x ∈ A φ) ∧
x ∈
A) → (φ ↔ ψ)) 

2.1.14 The empty set


Syntax  c0 3218 
Extend class notation to include the empty set.

class ∅ 

Definition  dfnul 3219 
Define the empty set. Special case of Exercise 4.10(o) of [Mendelson]
p. 231. For a more traditional definition, but requiring a dummy
variable, see dfnul2 3220. (Contributed by NM, 5Aug1993.)

⊢ ∅ = (V ∖ V) 

Theorem  dfnul2 3220 
Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring]
p. 20. (Contributed by NM, 26Dec1996.)

⊢ ∅ = {x ∣ ¬ x = x} 

Theorem  dfnul3 3221 
Alternate definition of the empty set. (Contributed by NM,
25Mar2004.)

⊢ ∅ = {x ∈ A ∣ ¬ x ∈ A} 

Theorem  noel 3222 
The empty set has no elements. Theorem 6.14 of [Quine] p. 44.
(Contributed by NM, 5Aug1993.) (Proof shortened by Mario Carneiro,
1Sep2015.)

⊢ ¬ A
∈ ∅ 

Theorem  n0i 3223 
If a set has elements, it is not empty. A set with elements is also
inhabited, see elex2 2564. (Contributed by NM, 31Dec1993.)

⊢ (B ∈ A →
¬ A = ∅) 

Theorem  ne0i 3224 
If a set has elements, it is not empty. A set with elements is also
inhabited, see elex2 2564. (Contributed by NM, 31Dec1993.)

⊢ (B ∈ A →
A ≠ ∅) 

Theorem  vn0 3225 
The universal class is not equal to the empty set. (Contributed by NM,
11Sep2008.)

⊢ V ≠ ∅ 

Theorem  vn0m 3226 
The universal class is inhabited. (Contributed by Jim Kingdon,
17Dec2018.)

⊢ ∃x x ∈ V 

Theorem  n0rf 3227 
An inhabited class is nonempty. Following the Definition of [Bauer],
p. 483, we call a class A nonempty if A ≠ ∅ and inhabited if
it has at least one element. In classical logic these two concepts are
equivalent, for example see Proposition 5.17(1) of [TakeutiZaring]
p. 20. This version of n0r 3228 requires only that x not be free in,
rather than not occur in, A. (Contributed by Jim Kingdon,
31Jul2018.)

⊢ ℲxA ⇒ ⊢ (∃x x ∈ A → A ≠
∅) 

Theorem  n0r 3228* 
An inhabited class is nonempty. See n0rf 3227 for more discussion.
(Contributed by Jim Kingdon, 31Jul2018.)

⊢ (∃x x ∈ A →
A ≠ ∅) 

Theorem  neq0r 3229* 
An inhabited class is nonempty. See n0rf 3227 for more discussion.
(Contributed by Jim Kingdon, 31Jul2018.)

⊢ (∃x x ∈ A →
¬ A = ∅) 

Theorem  reximdva0m 3230* 
Restricted existence deduced from inhabited class. (Contributed by Jim
Kingdon, 31Jul2018.)

⊢ ((φ
∧ x ∈ A) →
ψ) ⇒ ⊢ ((φ ∧ ∃x x ∈ A) → ∃x ∈ A ψ) 

Theorem  n0mmoeu 3231* 
A case of equivalence of "at most one" and "only one". If
a class is
inhabited, that class having at most one element is equivalent to it
having only one element. (Contributed by Jim Kingdon, 31Jul2018.)

⊢ (∃x x ∈ A →
(∃*x
x ∈
A ↔ ∃!x x ∈ A)) 

Theorem  rex0 3232 
Vacuous existential quantification is false. (Contributed by NM,
15Oct2003.)

⊢ ¬ ∃x ∈ ∅ φ 

Theorem  eq0 3233* 
The empty set has no elements. Theorem 2 of [Suppes] p. 22.
(Contributed by NM, 29Aug1993.)

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

Theorem  eqv 3234* 
The universe contains every set. (Contributed by NM, 11Sep2006.)

⊢ (A = V
↔ ∀x x ∈ A) 

Theorem  0el 3235* 
Membership of the empty set in another class. (Contributed by NM,
29Jun2004.)

⊢ (∅ ∈
A ↔ ∃x ∈ A ∀y ¬
y ∈
x) 

Theorem  abvor0dc 3236* 
The class builder of a decidable proposition not containing the
abstraction variable is either the universal class or the empty set.
(Contributed by Jim Kingdon, 1Aug2018.)

⊢ (DECID φ → ({x ∣ φ} = V ∨
{x ∣ φ} = ∅)) 

Theorem  abn0r 3237 
Nonempty class abstraction. (Contributed by Jim Kingdon,
1Aug2018.)

⊢ (∃xφ →
{x ∣ φ} ≠ ∅) 

Theorem  rabn0r 3238 
Nonempty restricted class abstraction. (Contributed by Jim Kingdon,
1Aug2018.)

⊢ (∃x ∈ A φ →
{x ∈
A ∣ φ} ≠ ∅) 

Theorem  rabn0m 3239* 
Inhabited restricted class abstraction. (Contributed by Jim Kingdon,
18Sep2018.)

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

Theorem  rab0 3240 
Any restricted class abstraction restricted to the empty set is empty.
(Contributed by NM, 15Oct2003.) (Proof shortened by Andrew Salmon,
26Jun2011.)

⊢ {x ∈ ∅ ∣ φ} = ∅ 

Theorem  rabeq0 3241 
Condition for a restricted class abstraction to be empty. (Contributed
by Jeff Madsen, 7Jun2010.)

⊢ ({x ∈ A ∣
φ} = ∅ ↔ ∀x ∈ A ¬
φ) 

Theorem  abeq0 3242 
Condition for a class abstraction to be empty. (Contributed by Jim
Kingdon, 12Aug2018.)

⊢ ({x ∣
φ} = ∅ ↔ ∀x ¬
φ) 

Theorem  rabxmdc 3243* 
Law of excluded middle given decidability, in terms of restricted class
abstractions. (Contributed by Jim Kingdon, 2Aug2018.)

⊢ (∀xDECID φ → A = ({x ∈ A ∣
φ} ∪ {x ∈ A ∣ ¬ φ})) 

Theorem  rabnc 3244* 
Law of noncontradiction, in terms of restricted class abstractions.
(Contributed by Jeff Madsen, 20Jun2011.)

⊢ ({x ∈ A ∣
φ} ∩ {x ∈ A ∣ ¬ φ}) = ∅ 

Theorem  un0 3245 
The union of a class with the empty set is itself. Theorem 24 of
[Suppes] p. 27. (Contributed by NM,
5Aug1993.)

⊢ (A ∪
∅) = A 

Theorem  in0 3246 
The intersection of a class with the empty set is the empty set.
Theorem 16 of [Suppes] p. 26.
(Contributed by NM, 5Aug1993.)

⊢ (A ∩
∅) = ∅ 

Theorem  inv1 3247 
The intersection of a class with the universal class is itself. Exercise
4.10(k) of [Mendelson] p. 231.
(Contributed by NM, 17May1998.)

⊢ (A ∩ V)
= A 

Theorem  unv 3248 
The union of a class with the universal class is the universal class.
Exercise 4.10(l) of [Mendelson] p. 231.
(Contributed by NM,
17May1998.)

⊢ (A ∪ V)
= V 

Theorem  0ss 3249 
The null set is a subset of any class. Part of Exercise 1 of
[TakeutiZaring] p. 22.
(Contributed by NM, 5Aug1993.)

⊢ ∅ ⊆ A 

Theorem  ss0b 3250 
Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its
converse. (Contributed by NM, 17Sep2003.)

⊢ (A ⊆
∅ ↔ A =
∅) 

Theorem  ss0 3251 
Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23.
(Contributed by NM, 13Aug1994.)

⊢ (A ⊆
∅ → A =
∅) 

Theorem  sseq0 3252 
A subclass of an empty class is empty. (Contributed by NM, 7Mar2007.)
(Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ ((A ⊆
B ∧
B = ∅) → A = ∅) 

Theorem  ssn0 3253 
A class with a nonempty subclass is nonempty. (Contributed by NM,
17Feb2007.)

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

Theorem  abf 3254 
A class builder with a false argument is empty. (Contributed by NM,
20Jan2012.)

⊢ ¬ φ ⇒ ⊢ {x ∣ φ} = ∅ 

Theorem  eq0rdv 3255* 
Deduction rule for equality to the empty set. (Contributed by NM,
11Jul2014.)

⊢ (φ
→ ¬ x ∈ A) ⇒ ⊢ (φ → A = ∅) 

Theorem  csbprc 3256 
The proper substitution of a proper class for a set into a class results
in the empty set. (Contributed by NM, 17Aug2018.)

⊢ (¬ A
∈ V → ⦋A / x⦌B = ∅) 

Theorem  un00 3257 
Two classes are empty iff their union is empty. (Contributed by NM,
11Aug2004.)

⊢ ((A =
∅ ∧ B = ∅) ↔ (A ∪ B) =
∅) 

Theorem  vss 3258 
Only the universal class has the universal class as a subclass.
(Contributed by NM, 17Sep2003.) (Proof shortened by Andrew Salmon,
26Jun2011.)

⊢ (V ⊆ A ↔ A =
V) 

Theorem  0pss 3259 
The null set is a proper subset of any nonempty set. (Contributed by NM,
27Feb1996.)

⊢ (∅ ⊊ A ↔ A ≠
∅) 

Theorem  npss0 3260 
No set is a proper subset of the empty set. (Contributed by NM,
17Jun1998.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ ¬ A
⊊ ∅ 

Theorem  pssv 3261 
Any nonuniversal class is a proper subclass of the universal class.
(Contributed by NM, 17May1998.)

⊢ (A ⊊
V ↔ ¬ A = V) 

Theorem  disj 3262* 
Two ways of saying that two classes are disjoint (have no members in
common). (Contributed by NM, 17Feb2004.)

⊢ ((A ∩
B) = ∅ ↔ ∀x ∈ A ¬
x ∈
B) 

Theorem  disjr 3263* 
Two ways of saying that two classes are disjoint. (Contributed by Jeff
Madsen, 19Jun2011.)

⊢ ((A ∩
B) = ∅ ↔ ∀x ∈ B ¬
x ∈
A) 

Theorem  disj1 3264* 
Two ways of saying that two classes are disjoint (have no members in
common). (Contributed by NM, 19Aug1993.)

⊢ ((A ∩
B) = ∅ ↔ ∀x(x ∈ A → ¬ x ∈ B)) 

Theorem  reldisj 3265 
Two ways of saying that two classes are disjoint, using the complement
of B
relative to a universe 𝐶. (Contributed by NM,
15Feb2007.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ (A ⊆
𝐶 → ((A ∩ B) =
∅ ↔ A ⊆ (𝐶 ∖ B))) 

Theorem  disj3 3266 
Two ways of saying that two classes are disjoint. (Contributed by NM,
19May1998.)

⊢ ((A ∩
B) = ∅ ↔ A = (A ∖
B)) 

Theorem  disjne 3267 
Members of disjoint sets are not equal. (Contributed by NM,
28Mar2007.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ (((A ∩
B) = ∅ ∧ 𝐶 ∈
A ∧ 𝐷 ∈ B) →
𝐶 ≠ 𝐷) 

Theorem  disjel 3268 
A set can't belong to both members of disjoint classes. (Contributed by
NM, 28Feb2015.)

⊢ (((A ∩
B) = ∅ ∧ 𝐶 ∈
A) → ¬ 𝐶 ∈
B) 

Theorem  disj2 3269 
Two ways of saying that two classes are disjoint. (Contributed by NM,
17May1998.)

⊢ ((A ∩
B) = ∅ ↔ A ⊆ (V ∖ B)) 

Theorem  disj4im 3270 
A consequence of two classes being disjoint. In classical logic this
would be a biconditional. (Contributed by Jim Kingdon, 2Aug2018.)

⊢ ((A ∩
B) = ∅ → ¬ (A ∖ B)
⊊ A) 

Theorem  ssdisj 3271 
Intersection with a subclass of a disjoint class. (Contributed by FL,
24Jan2007.)

⊢ ((A ⊆
B ∧
(B ∩ 𝐶) = ∅) → (A ∩ 𝐶) = ∅) 

Theorem  disjpss 3272 
A class is a proper subset of its union with a disjoint nonempty class.
(Contributed by NM, 15Sep2004.)

⊢ (((A ∩
B) = ∅ ∧ B ≠
∅) → A ⊊ (A ∪ B)) 

Theorem  undisj1 3273 
The union of disjoint classes is disjoint. (Contributed by NM,
26Sep2004.)

⊢ (((A ∩
𝐶) = ∅ ∧ (B ∩
𝐶) = ∅) ↔
((A ∪ B) ∩ 𝐶) = ∅) 

Theorem  undisj2 3274 
The union of disjoint classes is disjoint. (Contributed by NM,
13Sep2004.)

⊢ (((A ∩
B) = ∅ ∧ (A ∩
𝐶) = ∅) ↔
(A ∩ (B ∪ 𝐶)) = ∅) 

Theorem  ssindif0im 3275 
Subclass implies empty intersection with difference from the universal
class. (Contributed by NM, 17Sep2003.)

⊢ (A ⊆
B → (A ∩ (V ∖ B)) = ∅) 

Theorem  inelcm 3276 
The intersection of classes with a common member is nonempty.
(Contributed by NM, 7Apr1994.)

⊢ ((A ∈ B ∧ A ∈ 𝐶) → (B ∩ 𝐶) ≠ ∅) 

Theorem  minel 3277 
A minimum element of a class has no elements in common with the class.
(Contributed by NM, 22Jun1994.)

⊢ ((A ∈ B ∧ (𝐶 ∩ B) = ∅) → ¬ A ∈ 𝐶) 

Theorem  undif4 3278 
Distribute union over difference. (Contributed by NM, 17May1998.)
(Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ ((A ∩
𝐶) = ∅ →
(A ∪ (B ∖ 𝐶)) = ((A ∪ B)
∖ 𝐶)) 

Theorem  disjssun 3279 
Subset relation for disjoint classes. (Contributed by NM,
25Oct2005.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ ((A ∩
B) = ∅ → (A ⊆ (B
∪ 𝐶) ↔ A ⊆ 𝐶)) 

Theorem  ssdif0im 3280 
Subclass implies empty difference. One direction of Exercise 7 of
[TakeutiZaring] p. 22. In
classical logic this would be an
equivalence. (Contributed by Jim Kingdon, 2Aug2018.)

⊢ (A ⊆
B → (A ∖ B) =
∅) 

Theorem  vdif0im 3281 
Universal class equality in terms of empty difference. (Contributed by
Jim Kingdon, 3Aug2018.)

⊢ (A = V
→ (V ∖ A) =
∅) 

Theorem  difrab0eqim 3282* 
If the difference between the restricting class of a restricted class
abstraction and the restricted class abstraction is empty, the
restricting class is equal to this restricted class abstraction.
(Contributed by Jim Kingdon, 3Aug2018.)

⊢ (𝑉 = {x
∈ 𝑉 ∣ φ} → (𝑉 ∖ {x ∈ 𝑉 ∣ φ}) = ∅) 

Theorem  ssnelpss 3283 
A subclass missing a member is a proper subclass. (Contributed by NM,
12Jan2002.)

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

Theorem  ssnelpssd 3284 
Subclass inclusion with one element of the superclass missing is proper
subclass inclusion. Deduction form of ssnelpss 3283. (Contributed by
David Moews, 1May2017.)

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

Theorem  inssdif0im 3285 
Intersection, subclass, and difference relationship. In classical logic
the converse would also hold. (Contributed by Jim Kingdon,
3Aug2018.)

⊢ ((A ∩
B) ⊆ 𝐶 → (A ∩ (B
∖ 𝐶)) =
∅) 

Theorem  difid 3286 
The difference between a class and itself is the empty set. Proposition
5.15 of [TakeutiZaring] p. 20. Also
Theorem 32 of [Suppes] p. 28.
(Contributed by NM, 22Apr2004.)

⊢ (A ∖
A) = ∅ 

Theorem  difidALT 3287 
The difference between a class and itself is the empty set. Proposition
5.15 of [TakeutiZaring] p. 20.
Also Theorem 32 of [Suppes] p. 28.
Alternate proof of difid 3286. (Contributed by David Abernethy,
17Jun2012.) (Proof modification is discouraged.)
(New usage is discouraged.)

⊢ (A ∖
A) = ∅ 

Theorem  dif0 3288 
The difference between a class and the empty set. Part of Exercise 4.4 of
[Stoll] p. 16. (Contributed by NM,
17Aug2004.)

⊢ (A ∖
∅) = A 

Theorem  0dif 3289 
The difference between the empty set and a class. Part of Exercise 4.4 of
[Stoll] p. 16. (Contributed by NM,
17Aug2004.)

⊢ (∅ ∖ A) = ∅ 

Theorem  disjdif 3290 
A class and its relative complement are disjoint. Theorem 38 of [Suppes]
p. 29. (Contributed by NM, 24Mar1998.)

⊢ (A ∩
(B ∖ A)) = ∅ 

Theorem  difin0 3291 
The difference of a class from its intersection is empty. Theorem 37 of
[Suppes] p. 29. (Contributed by NM,
17Aug2004.) (Proof shortened by
Andrew Salmon, 26Jun2011.)

⊢ ((A ∩
B) ∖ B) = ∅ 

Theorem  undif1ss 3292 
Absorption of difference by union. In classical logic, as Theorem 35 of
[Suppes] p. 29, this would be equality
rather than subset. (Contributed
by Jim Kingdon, 4Aug2018.)

⊢ ((A ∖
B) ∪ B) ⊆ (A
∪ B) 

Theorem  undif2ss 3293 
Absorption of difference by union. In classical logic, as in Part of
proof of Corollary 6K of [Enderton] p.
144, this would be equality rather
than subset. (Contributed by Jim Kingdon, 4Aug2018.)

⊢ (A ∪
(B ∖ A)) ⊆ (A
∪ B) 

Theorem  undifabs 3294 
Absorption of difference by union. (Contributed by NM, 18Aug2013.)

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

Theorem  inundifss 3295 
The intersection and class difference of a class with another class are
contained in the original class. In classical logic we'd be able to make
a stronger statement: that everything in the original class is in the
intersection or the difference (that is, this theorem would be equality
rather than subset). (Contributed by Jim Kingdon, 4Aug2018.)

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

Theorem  difun2 3296 
Absorption of union by difference. Theorem 36 of [Suppes] p. 29.
(Contributed by NM, 19May1998.)

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

Theorem  undifss 3297 
Union of complementary parts into whole. (Contributed by Jim Kingdon,
4Aug2018.)

⊢ (A ⊆
B ↔ (A ∪ (B
∖ A)) ⊆ B) 

Theorem  ssdifin0 3298 
A subset of a difference does not intersect the subtrahend. (Contributed
by Jeff Hankins, 1Sep2013.) (Proof shortened by Mario Carneiro,
24Aug2015.)

⊢ (A ⊆
(B ∖ 𝐶) → (A ∩ 𝐶) = ∅) 

Theorem  ssdifeq0 3299 
A class is a subclass of itself subtracted from another iff it is the
empty set. (Contributed by Steve Rodriguez, 20Nov2015.)

⊢ (A ⊆
(B ∖ A) ↔ A =
∅) 

Theorem  ssundifim 3300 
A consequence of inclusion in the union of two classes. In classical
logic this would be a biconditional. (Contributed by Jim Kingdon,
4Aug2018.)

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