Type  Label  Description 
Statement 

Theorem  difabs 3201 
Absorptionlike law for class difference: you can remove a class only
once. (Contributed by FL, 2Aug2009.)

⊢ ((𝐴 ∖ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) 

Theorem  symdif1 3202 
Two ways to express symmetric difference. This theorem shows the
equivalence of the definition of symmetric difference in [Stoll] p. 13 and
the restated definition in Example 4.1 of [Stoll] p. 262. (Contributed by
NM, 17Aug2004.)

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

2.1.13.5 Class abstractions with difference,
union, and intersection of two classes


Theorem  symdifxor 3203* 
Expressing symmetric difference with exclusiveor or two differences.
(Contributed by Jim Kingdon, 28Jul2018.)

⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)) = {𝑥 ∣ (𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ 𝐵)} 

Theorem  unab 3204 
Union of two class abstractions. (Contributed by NM, 29Sep2002.)
(Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∨ 𝜓)} 

Theorem  inab 3205 
Intersection of two class abstractions. (Contributed by NM,
29Sep2002.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ ({𝑥 ∣ 𝜑} ∩ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ 𝜓)} 

Theorem  difab 3206 
Difference of two class abstractions. (Contributed by NM, 23Oct2004.)
(Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ ({𝑥 ∣ 𝜑} ∖ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ ¬ 𝜓)} 

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

⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑥 ∣ 𝜑}) 

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

⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)} 

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

⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} 

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

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

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

⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ ¬ 𝜓)} 

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

⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = ({𝑥 ∣ 𝜑} ∩ 𝐴) 

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

⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∣ 𝜑}) 

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

⊢ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝜑}) = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} 

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

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

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

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

2.1.13.6 Restricted uniqueness with difference,
union, and intersection


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

⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑) 

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

⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → ∃!𝑥 ∈ 𝐴 𝜑) 

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

⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ (𝐴 ∪ 𝐵)(𝜑 ∨ 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑) 

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

⊢ (¬ ∃𝑥 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜑)) 

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

⊢ (((𝐴 ⊆ 𝐵 ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑)) ∧ 𝜑) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) 

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

⊢ ((∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓)) 

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

⊢ (((∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) ∧ ∃𝑥 ∈ 𝐴 𝜓 ∧ ∃!𝑥 ∈ 𝐴 𝜑) ∧ 𝑥 ∈ 𝐴) → (𝜑 ↔ 𝜓)) 

2.1.14 The empty set


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

class ∅ 

Definition  dfnul 3225 
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 3226. (Contributed by NM, 5Aug1993.)

⊢ ∅ = (V ∖ V) 

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

⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥} 

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

⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴} 

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

⊢ ¬ 𝐴 ∈ ∅ 

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

⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅) 

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

⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅) 

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

⊢ V ≠ ∅ 

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

⊢ ∃𝑥 𝑥 ∈ V 

Theorem  n0rf 3233 
An inhabited class is nonempty. Following the Definition of [Bauer],
p. 483, we call a class 𝐴 nonempty if 𝐴 ≠ ∅ 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 3234 requires only that 𝑥 not be free in,
rather than not occur in, 𝐴. (Contributed by Jim Kingdon,
31Jul2018.)

⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∃𝑥 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅) 

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

⊢ (∃𝑥 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅) 

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

⊢ (∃𝑥 𝑥 ∈ 𝐴 → ¬ 𝐴 = ∅) 

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

⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ ((𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 𝜓) 

Theorem  n0mmoeu 3237* 
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.)

⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 𝑥 ∈ 𝐴)) 

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

⊢ ¬ ∃𝑥 ∈ ∅ 𝜑 

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

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

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

⊢ (𝐴 = V ↔ ∀𝑥 𝑥 ∈ 𝐴) 

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

⊢ (∅ ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ¬ 𝑦 ∈ 𝑥) 

Theorem  abvor0dc 3242* 
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 𝜑 → ({𝑥 ∣ 𝜑} = V ∨ {𝑥 ∣ 𝜑} = ∅)) 

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

⊢ (∃𝑥𝜑 → {𝑥 ∣ 𝜑} ≠ ∅) 

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

⊢ (∃𝑥 ∈ 𝐴 𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅) 

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

⊢ (∃𝑦 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐴 𝜑) 

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

⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅ 

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

⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) 

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

⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑) 

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

⊢ (∀𝑥DECID 𝜑 → 𝐴 = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑})) 

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

⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) = ∅ 

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

⊢ (𝐴 ∪ ∅) = 𝐴 

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

⊢ (𝐴 ∩ ∅) = ∅ 

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

⊢ (𝐴 ∩ V) = 𝐴 

Theorem  unv 3254 
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.)

⊢ (𝐴 ∪ V) = V 

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

⊢ ∅ ⊆ 𝐴 

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

⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) 

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

⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) 

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

⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅) 

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

⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅) 

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

⊢ ¬ 𝜑 ⇒ ⊢ {𝑥 ∣ 𝜑} = ∅ 

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

⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = ∅) 

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

⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅) 

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

⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 ∪ 𝐵) = ∅) 

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

⊢ (V ⊆ 𝐴 ↔ 𝐴 = V) 

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

⊢ (∅ ⊊ 𝐴 ↔ 𝐴 ≠ ∅) 

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

⊢ ¬ 𝐴 ⊊ ∅ 

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

⊢ (𝐴 ⊊ V ↔ ¬ 𝐴 = V) 

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

⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) 

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

⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ 𝐴) 

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

⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) 

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

⊢ (𝐴 ⊆ 𝐶 → ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶 ∖ 𝐵))) 

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

⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 = (𝐴 ∖ 𝐵)) 

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

⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → 𝐶 ≠ 𝐷) 

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

⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴) → ¬ 𝐶 ∈ 𝐵) 

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

⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (V ∖ 𝐵)) 

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

⊢ ((𝐴 ∩ 𝐵) = ∅ → ¬ (𝐴 ∖ 𝐵) ⊊ 𝐴) 

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

⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (𝐴 ∩ 𝐶) = ∅) 

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

⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐵 ≠ ∅) → 𝐴 ⊊ (𝐴 ∪ 𝐵)) 

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

⊢ (((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐶) = ∅) ↔ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ∅) 

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

⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ (𝐴 ∩ 𝐶) = ∅) ↔ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ∅) 

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

⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ (V ∖ 𝐵)) = ∅) 

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

⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅) 

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

⊢ ((𝐴 ∈ 𝐵 ∧ (𝐶 ∩ 𝐵) = ∅) → ¬ 𝐴 ∈ 𝐶) 

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

⊢ ((𝐴 ∩ 𝐶) = ∅ → (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)) 

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

⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ 𝐴 ⊆ 𝐶)) 

Theorem  ssdif0im 3286 
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.)

⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐵) = ∅) 

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

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

Theorem  difrab0eqim 3288* 
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.)

⊢ (𝑉 = {𝑥 ∈ 𝑉 ∣ 𝜑} → (𝑉 ∖ {𝑥 ∈ 𝑉 ∣ 𝜑}) = ∅) 

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

⊢ (𝐴 ⊆ 𝐵 → ((𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴) → 𝐴 ⊊ 𝐵)) 

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

⊢ (𝜑 → 𝐴 ⊆ 𝐵)
& ⊢ (𝜑 → 𝐶 ∈ 𝐵)
& ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ⊊ 𝐵) 

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

⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐶 → (𝐴 ∩ (𝐵 ∖ 𝐶)) = ∅) 

Theorem  difid 3292 
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.)

⊢ (𝐴 ∖ 𝐴) = ∅ 

Theorem  difidALT 3293 
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 3292. (Contributed by David Abernethy,
17Jun2012.) (Proof modification is discouraged.)
(New usage is discouraged.)

⊢ (𝐴 ∖ 𝐴) = ∅ 

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

⊢ (𝐴 ∖ ∅) = 𝐴 

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

⊢ (∅ ∖ 𝐴) = ∅ 

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

⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ 

Theorem  difin0 3297 
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.)

⊢ ((𝐴 ∩ 𝐵) ∖ 𝐵) = ∅ 

Theorem  undif1ss 3298 
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.)

⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) ⊆ (𝐴 ∪ 𝐵) 

Theorem  undif2ss 3299 
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.)

⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) ⊆ (𝐴 ∪ 𝐵) 

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

⊢ (𝐴 ∪ (𝐴 ∖ 𝐵)) = 𝐴 