Type  Label  Description 
Statement 

Theorem  indi 3501 
Distributive law for intersection over union. Exercise 10 of
[TakeutiZaring] p. 17.
(Contributed by NM, 30Sep2002.) (Proof
shortened by Andrew Salmon, 26Jun2011.)

⊢ (A ∩
(B ∪ C)) = ((A ∩
B) ∪ (A ∩ C)) 

Theorem  undi 3502 
Distributive law for union over intersection. Exercise 11 of
[TakeutiZaring] p. 17.
(Contributed by NM, 30Sep2002.) (Proof
shortened by Andrew Salmon, 26Jun2011.)

⊢ (A ∪
(B ∩ C)) = ((A ∪
B) ∩ (A ∪ C)) 

Theorem  indir 3503 
Distributive law for intersection over union. Theorem 28 of [Suppes]
p. 27. (Contributed by NM, 30Sep2002.)

⊢ ((A ∪
B) ∩ C) = ((A ∩
C) ∪ (B ∩ C)) 

Theorem  undir 3504 
Distributive law for union over intersection. Theorem 29 of [Suppes]
p. 27. (Contributed by NM, 30Sep2002.)

⊢ ((A ∩
B) ∪ C) = ((A ∪
C) ∩ (B ∪ C)) 

Theorem  unineq 3505 
Infer equality from equalities of union and intersection. Exercise 20
of [Enderton] p. 32 and its converse.
(Contributed by NM,
10Aug2004.)

⊢ (((A ∪
C) = (B ∪ C)
∧ (A
∩ C) = (B ∩ C))
↔ A = B) 

Theorem  uneqin 3506 
Equality of union and intersection implies equality of their arguments.
(Contributed by NM, 16Apr2006.) (Proof shortened by Andrew Salmon,
26Jun2011.)

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

Theorem  difundi 3507 
Distributive law for class difference. Theorem 39 of [Suppes] p. 29.
(Contributed by NM, 17Aug2004.)

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

Theorem  difundir 3508 
Distributive law for class difference. (Contributed by NM,
17Aug2004.)

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

Theorem  difindi 3509 
Distributive law for class difference. Theorem 40 of [Suppes] p. 29.
(Contributed by NM, 17Aug2004.)

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

Theorem  difindir 3510 
Distributive law for class difference. (Contributed by NM,
17Aug2004.)

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

Theorem  indifdir 3511 
Distribute intersection over difference. (Contributed by Scott Fenton,
14Apr2011.)

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

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

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

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

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

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

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

Theorem  undif3 3515 
An equality involving class union and class difference. The first
equality of Exercise 13 of [TakeutiZaring] p. 22. (Contributed by Alan
Sare, 17Apr2012.)

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

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

⊢ (A ⊆ C →
(A ∖
B) = ((C ∖ B) ∩ A)) 

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

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

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

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

Theorem  symdif1 3519 
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.)

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

Theorem  symdif2 3520* 
Two ways to express symmetric difference. (Contributed by NM,
17Aug2004.) (Proof shortened by Andrew Salmon, 26Jun2011.)

⊢ ((A ∖ B) ∪
(B ∖
A)) = {x ∣ ¬
(x ∈
A ↔ x ∈ B)} 

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

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

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

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

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

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

Theorem  complab 3524 
Complement of a class abstraction. (Contributed by SF, 12Jan2015.)

⊢ ∼ {x
∣ φ} = {x
∣ ¬ φ} 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem  dfrab3ss 3533* 
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 3534 
Abstraction restricted to a union. (Contributed by Stefan O'Rear,
5Feb2015.)

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem  reupick2 3541* 
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) → (φ ↔ ψ)) 

Theorem  symdifcom 3542 
Symmetric difference commutes. (Contributed by SF, 11Jan2015.)

⊢ (A ⊕
B) = (B ⊕ A) 

Theorem  compleqb 3543 
Two classes are equal iff their complements are equal. (Contributed by
SF, 11Jan2015.)

⊢ (A =
B ↔ ∼ A = ∼ B) 

Theorem  necompl 3544 
A class is not equal to its complement. (Contributed by SF,
11Jan2015.)

⊢ ∼ A
≠ A 

Theorem  dfin5 3545 
Definition of intersection in terms of union. (Contributed by SF,
12Jan2015.)

⊢ (A ∩
B) = ∼ ( ∼ A ∪ ∼ B) 

Theorem  dfun4 3546 
Definition of union in terms of intersection. (Contributed by SF,
12Jan2015.)

⊢ (A ∪
B) = ∼ ( ∼ A ∩ ∼ B) 

Theorem  iunin 3547 
Intersection of two complements is equal to the complement of a union.
(Contributed by SF, 12Jan2015.)

⊢ ∼ (A
∪ B) = ( ∼ A ∩ ∼ B) 

Theorem  iinun 3548 
Complement of intersection is equal to union of complements. (Contributed
by SF, 12Jan2015.)

⊢ ∼ (A
∩ B) = ( ∼ A ∪ ∼ B) 

Theorem  difsscompl 3549 
A difference is a subset of the complement of its second argument.
(Contributed by SF, 10Mar2015.)

⊢ (A ∖ B) ⊆ ∼ B 

2.1.13 The empty set


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

class
∅ 

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

⊢ ∅ = (V ∖ V) 

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

⊢ ∅ =
{x ∣
¬ x = x} 

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

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

Theorem  noel 3554 
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 3555 
If a set has elements, it is not empty. (Contributed by NM,
31Dec1993.)

⊢ (B ∈ A →
¬ A = ∅) 

Theorem  ne0i 3556 
If a set has elements, it is not empty. (Contributed by NM,
31Dec1993.)

⊢ (B ∈ A →
A ≠ ∅) 

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

⊢ V ≠ ∅ 

Theorem  n0f 3558 
A nonempty class has at least one element. Proposition 5.17(1) of
[TakeutiZaring] p. 20. This
version of n0 3559 requires only that x
not be free in, rather than not occur in, A. (Contributed by NM,
17Oct2003.)

⊢ F/_xA ⇒ ⊢ (A ≠
∅ ↔ ∃x x ∈ A) 

Theorem  n0 3559* 
A nonempty class has at least one element. Proposition 5.17(1) of
[TakeutiZaring] p. 20.
(Contributed by NM, 29Sep2006.)

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

Theorem  neq0 3560* 
A nonempty class has at least one element. Proposition 5.17(1) of
[TakeutiZaring] p. 20.
(Contributed by NM, 5Aug1993.)

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

Theorem  reximdva0 3561* 
Restricted existence deduced from nonempty class. (Contributed by NM,
1Feb2012.)

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

Theorem  n0moeu 3562* 
A case of equivalence of "at most one" and "only one".
(Contributed by
FL, 6Dec2010.)

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

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

⊢ ¬ ∃x ∈ ∅ φ 

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

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

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

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

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

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

Theorem  abvor0 3567* 
The class builder of a wff not containing the abstraction variable is
either the universal class or the empty set. (Contributed by Mario
Carneiro, 29Aug2013.)

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

Theorem  abn0 3568 
Nonempty class abstraction. (Contributed by NM, 26Dec1996.) (Proof
shortened by Mario Carneiro, 11Nov2016.)

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

Theorem  ab0 3569 
Empty class abstraction. (Contributed by SF, 5Jan2018.)

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

Theorem  rabn0 3570 
Nonempty restricted class abstraction. (Contributed by NM,
29Aug1999.)

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

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

⊢ {x ∈ ∅ ∣ φ} =
∅ 

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

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

Theorem  rabxm 3573* 
Law of excluded middle, in terms of restricted class abstractions.
(Contributed by Jeff Madsen, 20Jun2011.)

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

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

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

Theorem  un0 3575 
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 3576 
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 3577 
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 3578 
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 3579 
The null set is a subset of any class. Part of Exercise 1 of
[TakeutiZaring] p. 22.
(Contributed by NM, 5Aug1993.)

⊢ ∅ ⊆ A 

Theorem  ss0b 3580 
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 3581 
Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23.
(Contributed by NM, 13Aug1994.)

⊢ (A ⊆ ∅ →
A = ∅) 

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

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

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

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

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

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

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

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

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

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

Theorem  vss 3587 
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 3588 
The null set is a proper subset of any nonempty set. (Contributed by NM,
27Feb1996.)

⊢ (∅ ⊂ A ↔
A ≠ ∅) 

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

⊢ ¬ A
⊂ ∅ 

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

⊢ (A ⊂ V ↔ ¬ A = V) 

Theorem  disj 3591* 
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 3592* 
Two ways of saying that two classes are disjoint. (Contributed by Jeff
Madsen, 19Jun2011.)

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

Theorem  disj1 3593* 
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 3594 
Two ways of saying that two classes are disjoint, using the complement
of B relative to a
universe C. (Contributed by
NM,
15Feb2007.) (Proof shortened by Andrew Salmon, 26Jun2011.)

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

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

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

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

⊢ (((A ∩
B) = ∅
∧ C ∈ A ∧ D ∈ B) →
C ≠ D) 

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

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

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

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

Theorem  disj4 3599 
Two ways of saying that two classes are disjoint. (Contributed by NM,
21Mar2004.)

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

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

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