Type  Label  Description 
Statement 

Theorem  difdif2ss 3301 
Set difference with a set difference. In classical logic this would be
equality rather than subset. (Contributed by Jim Kingdon,
27Jul2018.)

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

Theorem  undm 3302 
De Morgan's law for union. Theorem 5.2(13) of [Stoll] p. 19.
(Contributed by NM, 18Aug2004.)

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

Theorem  indmss 3303 
De Morgan's law for intersection. In classical logic, this would be
equality rather than subset, as in Theorem 5.2(13') of [Stoll] p. 19.
(Contributed by Jim Kingdon, 27Jul2018.)

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

Theorem  difun1 3304 
A relationship involving double difference and union. (Contributed by NM,
29Aug2004.)

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

Theorem  undif3ss 3305 
A subset relationship involving class union and class difference. In
classical logic, this would be equality rather than subset, as in the
first equality of Exercise 13 of [TakeutiZaring] p. 22. (Contributed by
Jim Kingdon, 28Jul2018.)

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

Theorem  difin2 3306 
Represent a set difference as an intersection with a larger difference.
(Contributed by Jeff Madsen, 2Sep2009.)

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

Theorem  dif32 3307 
Swap second and third argument of double difference. (Contributed by NM,
18Aug2004.)

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

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

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

Theorem  symdif1 3309 
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 3310* 
Expressing symmetric difference with exclusiveor or two differences.
(Contributed by Jim Kingdon, 28Jul2018.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2.1.13.6 Restricted uniqueness with difference,
union, and intersection


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

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

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

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

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

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

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

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

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

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

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

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

Theorem  reupick2 3330* 
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 3331 
Extend class notation to include the empty set.

class ∅ 

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

⊢ ∅ = (V ∖ V) 

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

⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥} 

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

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

Theorem  noel 3335 
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 3336 
If a set has elements, it is not empty. A set with elements is also
inhabited, see elex2 2674. (Contributed by NM, 31Dec1993.)

⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅) 

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

⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅) 

Theorem  ne0d 3338 
Deduction form of ne0i 3337. If a class has elements, then it is
nonempty. (Contributed by Glauco Siliprandi, 23Oct2021.)

⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≠ ∅) 

Theorem  n0ii 3339 
If a class has elements, then it is not empty. Inference associated
with n0i 3336. (Contributed by BJ, 15Jul2021.)

⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ¬ 𝐵 = ∅ 

Theorem  ne0ii 3340 
If a class has elements, then it is nonempty. Inference associated with
ne0i 3337. (Contributed by Glauco Siliprandi,
11Dec2019.)

⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐵 ≠ ∅ 

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

⊢ V ≠ ∅ 

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

⊢ ∃𝑥 𝑥 ∈ V 

Theorem  n0rf 3343 
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 3344 requires only that 𝑥 not be free in,
rather than not occur in, 𝐴. (Contributed by Jim Kingdon,
31Jul2018.)

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

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

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

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

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

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

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

Theorem  n0mmoeu 3347* 
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 3348 
Vacuous existential quantification is false. (Contributed by NM,
15Oct2003.)

⊢ ¬ ∃𝑥 ∈ ∅ 𝜑 

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

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

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

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

Theorem  notm0 3351* 
A class is not inhabited if and only if it is empty. (Contributed by
Jim Kingdon, 1Jul2022.)

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

Theorem  nel0 3352* 
From the general negation of membership in 𝐴, infer that 𝐴 is
the empty set. (Contributed by BJ, 6Oct2018.)

⊢ ¬ 𝑥 ∈ 𝐴 ⇒ ⊢ 𝐴 = ∅ 

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

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

Theorem  abvor0dc 3354* 
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 3355 
Nonempty class abstraction. (Contributed by Jim Kingdon, 1Aug2018.)

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

Theorem  abn0m 3356* 
Inhabited class abstraction. (Contributed by Jim Kingdon,
8Jul2022.)

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

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

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

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

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

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

⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅ 

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

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

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

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

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

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

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

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

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

⊢ (𝐴 ∪ ∅) = 𝐴 

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

⊢ (𝐴 ∩ ∅) = ∅ 

Theorem  0in 3366 
The intersection of the empty set with a class is the empty set.
(Contributed by Glauco Siliprandi, 17Aug2020.)

⊢ (∅ ∩ 𝐴) = ∅ 

Theorem  inv1 3367 
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 3368 
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 3369 
The null set is a subset of any class. Part of Exercise 1 of
[TakeutiZaring] p. 22.
(Contributed by NM, 5Aug1993.)

⊢ ∅ ⊆ 𝐴 

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

⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) 

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

⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) 

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

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

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

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

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

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

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

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

Theorem  csbprc 3376 
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 3377 
Two classes are empty iff their union is empty. (Contributed by NM,
11Aug2004.)

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

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

⊢ (V ⊆ 𝐴 ↔ 𝐴 = V) 

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

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

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

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

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

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

Theorem  reldisj 3382 
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 3383 
Two ways of saying that two classes are disjoint. (Contributed by NM,
19May1998.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem  ssdif0im 3395 
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 3396 
Universal class equality in terms of empty difference. (Contributed by
Jim Kingdon, 3Aug2018.)

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

Theorem  difrab0eqim 3397* 
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  inssdif0im 3398 
Intersection, subclass, and difference relationship. In classical logic
the converse would also hold. (Contributed by Jim Kingdon,
3Aug2018.)

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

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

⊢ (𝐴 ∖ 𝐴) = ∅ 