Type  Label  Description 
Statement 

Theorem  preq12 3801 
Equality theorem for unordered pairs. (Contributed by NM,
19Oct2012.)

⊢ ((A =
C ∧
B = D)
→ {A, B} = {C,
D}) 

Theorem  preq1i 3802 
Equality inference for unordered pairs. (Contributed by NM,
19Oct2012.)

⊢ A =
B ⇒ ⊢ {A,
C} = {B, C} 

Theorem  preq2i 3803 
Equality inference for unordered pairs. (Contributed by NM,
19Oct2012.)

⊢ A =
B ⇒ ⊢ {C,
A} = {C, B} 

Theorem  preq12i 3804 
Equality inference for unordered pairs. (Contributed by NM,
19Oct2012.)

⊢ A =
B
& ⊢ C =
D ⇒ ⊢ {A,
C} = {B, D} 

Theorem  preq1d 3805 
Equality deduction for unordered pairs. (Contributed by NM,
19Oct2012.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ {A, C} = {B,
C}) 

Theorem  preq2d 3806 
Equality deduction for unordered pairs. (Contributed by NM,
19Oct2012.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ {C, A} = {C,
B}) 

Theorem  preq12d 3807 
Equality deduction for unordered pairs. (Contributed by NM,
19Oct2012.)

⊢ (φ
→ A = B)
& ⊢ (φ
→ C = D) ⇒ ⊢ (φ
→ {A, C} = {B,
D}) 

Theorem  tpeq1 3808 
Equality theorem for unordered triples. (Contributed by NM,
13Sep2011.)

⊢ (A =
B → {A, C, D} = {B,
C, D}) 

Theorem  tpeq2 3809 
Equality theorem for unordered triples. (Contributed by NM,
13Sep2011.)

⊢ (A =
B → {C, A, D} = {C,
B, D}) 

Theorem  tpeq3 3810 
Equality theorem for unordered triples. (Contributed by NM,
13Sep2011.)

⊢ (A =
B → {C, D, A} = {C,
D, B}) 

Theorem  tpeq1d 3811 
Equality theorem for unordered triples. (Contributed by NM,
22Jun2014.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ {A, C, D} =
{B, C,
D}) 

Theorem  tpeq2d 3812 
Equality theorem for unordered triples. (Contributed by NM,
22Jun2014.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ {C, A, D} =
{C, B,
D}) 

Theorem  tpeq3d 3813 
Equality theorem for unordered triples. (Contributed by NM,
22Jun2014.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ {C, D, A} =
{C, D,
B}) 

Theorem  tpeq123d 3814 
Equality theorem for unordered triples. (Contributed by NM,
22Jun2014.)

⊢ (φ
→ A = B)
& ⊢ (φ
→ C = D)
& ⊢ (φ
→ E = F) ⇒ ⊢ (φ
→ {A, C, E} =
{B, D,
F}) 

Theorem  tprot 3815 
Rotation of the elements of an unordered triple. (Contributed by Alan
Sare, 24Oct2011.)

⊢ {A,
B, C}
= {B, C, A} 

Theorem  tpcoma 3816 
Swap 1st and 2nd members of an undordered triple. (Contributed by NM,
22May2015.)

⊢ {A,
B, C}
= {B, A, C} 

Theorem  tpcomb 3817 
Swap 2nd and 3rd members of an undordered triple. (Contributed by NM,
22May2015.)

⊢ {A,
B, C}
= {A, C, B} 

Theorem  tpass 3818 
Split off the first element of an unordered triple. (Contributed by Mario
Carneiro, 5Jan2016.)

⊢ {A,
B, C}
= ({A} ∪ {B, C}) 

Theorem  qdass 3819 
Two ways to write an unordered quadruple. (Contributed by Mario Carneiro,
5Jan2016.)

⊢ ({A,
B} ∪ {C, D}) =
({A, B, C} ∪
{D}) 

Theorem  qdassr 3820 
Two ways to write an unordered quadruple. (Contributed by Mario Carneiro,
5Jan2016.)

⊢ ({A,
B} ∪ {C, D}) =
({A} ∪ {B, C, D}) 

Theorem  tpidm12 3821 
Unordered triple {A, A, B} is
just an overlong way to write
{A, B}. (Contributed by David A. Wheeler,
10May2015.)

⊢ {A,
A, B}
= {A, B} 

Theorem  tpidm13 3822 
Unordered triple {A, B, A} is
just an overlong way to write
{A, B}. (Contributed by David A. Wheeler,
10May2015.)

⊢ {A,
B, A}
= {A, B} 

Theorem  tpidm23 3823 
Unordered triple {A, B, B} is
just an overlong way to write
{A, B}. (Contributed by David A. Wheeler,
10May2015.)

⊢ {A,
B, B}
= {A, B} 

Theorem  tpidm 3824 
Unordered triple {A, A, A} is
just an overlong way to write
{A}. (Contributed by
David A. Wheeler, 10May2015.)

⊢ {A,
A, A}
= {A} 

Theorem  prid1g 3825 
An unordered pair contains its first member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by Stefan
Allan, 8Nov2008.)

⊢ (A ∈ V →
A ∈
{A, B}) 

Theorem  prid2g 3826 
An unordered pair contains its second member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by Stefan
Allan, 8Nov2008.)

⊢ (B ∈ V →
B ∈
{A, B}) 

Theorem  prid1 3827 
An unordered pair contains its first member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by NM,
5Aug1993.)

⊢ A ∈ V ⇒ ⊢ A ∈ {A, B} 

Theorem  prid2 3828 
An unordered pair contains its second member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by NM,
5Aug1993.)

⊢ B ∈ V ⇒ ⊢ B ∈ {A, B} 

Theorem  tpid1 3829 
One of the three elements of an unordered triple. (Contributed by NM,
7Apr1994.) (Proof shortened by Andrew Salmon, 29Jun2011.)

⊢ A ∈ V ⇒ ⊢ A ∈ {A, B, C} 

Theorem  tpid2 3830 
One of the three elements of an unordered triple. (Contributed by NM,
7Apr1994.) (Proof shortened by Andrew Salmon, 29Jun2011.)

⊢ B ∈ V ⇒ ⊢ B ∈ {A, B, C} 

Theorem  tpid3g 3831 
Closed theorem form of tpid3 3832. This proof was automatically generated
from the virtual deduction proof tpid3gVD (future) using
a translation
program. (Contributed by Alan Sare, 24Oct2011.)

⊢ (A ∈ B →
A ∈
{C, D,
A}) 

Theorem  tpid3 3832 
One of the three elements of an unordered triple. (Contributed by NM,
7Apr1994.) (Proof shortened by Andrew Salmon, 29Jun2011.)

⊢ C ∈ V ⇒ ⊢ C ∈ {A, B, C} 

Theorem  snnzg 3833 
The singleton of a set is not empty. (Contributed by NM, 14Dec2008.)

⊢ (A ∈ V →
{A} ≠ ∅) 

Theorem  snnz 3834 
The singleton of a set is not empty. (Contributed by NM,
10Apr1994.)

⊢ A ∈ V ⇒ ⊢ {A} ≠
∅ 

Theorem  prnz 3835 
A pair containing a set is not empty. (Contributed by NM,
9Apr1994.)

⊢ A ∈ V ⇒ ⊢ {A,
B} ≠ ∅ 

Theorem  prnzg 3836 
A pair containing a set is not empty. (Contributed by FL,
19Sep2011.)

⊢ (A ∈ V →
{A, B}
≠ ∅) 

Theorem  tpnz 3837 
A triplet containing a set is not empty. (Contributed by NM,
10Apr1994.)

⊢ A ∈ V ⇒ ⊢ {A,
B, C}
≠ ∅ 

Theorem  snss 3838 
The singleton of an element of a class is a subset of the class.
Theorem 7.4 of [Quine] p. 49.
(Contributed by NM, 5Aug1993.)

⊢ A ∈ V ⇒ ⊢ (A ∈ B ↔
{A} ⊆
B) 

Theorem  eldifsn 3839 
Membership in a set with an element removed. (Contributed by NM,
10Oct2007.)

⊢ (A ∈ (B ∖ {C}) ↔
(A ∈
B ∧
A ≠ C)) 

Theorem  eldifsni 3840 
Membership in a set with an element removed. (Contributed by NM,
10Mar2015.)

⊢ (A ∈ (B ∖ {C}) →
A ≠ C) 

Theorem  neldifsn 3841 
A is not in (B ∖ {A}). (Contributed by David Moews,
1May2017.)

⊢ ¬ A
∈ (B
∖ {A}) 

Theorem  neldifsnd 3842 
A is not in (B ∖ {A}). Deduction form. (Contributed by
David Moews, 1May2017.)

⊢ (φ
→ ¬ A ∈ (B ∖ {A})) 

Theorem  rexdifsn 3843 
Restricted existential quantification over a set with an element removed.
(Contributed by NM, 4Feb2015.)

⊢ (∃x ∈ (A ∖ {B})φ ↔
∃x
∈ A
(x ≠ B ∧ φ)) 

Theorem  snssg 3844 
The singleton of an element of a class is a subset of the class.
Theorem 7.4 of [Quine] p. 49.
(Contributed by NM, 22Jul2001.)

⊢ (A ∈ V →
(A ∈
B ↔ {A} ⊆ B)) 

Theorem  difsn 3845 
An element not in a set can be removed without affecting the set.
(Contributed by NM, 16Mar2006.) (Proof shortened by Andrew Salmon,
29Jun2011.)

⊢ (¬ A
∈ B
→ (B ∖ {A}) =
B) 

Theorem  difprsnss 3846 
Removal of a singleton from an unordered pair. (Contributed by NM,
16Mar2006.) (Proof shortened by Andrew Salmon, 29Jun2011.)

⊢ ({A,
B} ∖
{A}) ⊆
{B} 

Theorem  difprsn1 3847 
Removal of a singleton from an unordered pair. (Contributed by Thierry
Arnoux, 4Feb2017.)

⊢ (A ≠
B → ({A, B} ∖ {A}) =
{B}) 

Theorem  difprsn2 3848 
Removal of a singleton from an unordered pair. (Contributed by Alexander
van der Vekens, 5Oct2017.)

⊢ (A ≠
B → ({A, B} ∖ {B}) =
{A}) 

Theorem  diftpsn3 3849 
Removal of a singleton from an unordered triple. (Contributed by
Alexander van der Vekens, 5Oct2017.)

⊢ ((A ≠
C ∧
B ≠ C) → ({A,
B, C}
∖ {C})
= {A, B}) 

Theorem  difsnb 3850 
(B ∖ {A})
equals B if and only if A is not a member of
B. Generalization of difsn 3845. (Contributed by David Moews,
1May2017.)

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

Theorem  difsnpss 3851 
(B ∖ {A})
is a proper subclass of B if
and only if A is a
member of B.
(Contributed by David Moews, 1May2017.)

⊢ (A ∈ B ↔
(B ∖
{A}) ⊂
B) 

Theorem  snssi 3852 
The singleton of an element of a class is a subset of the class.
(Contributed by NM, 6Jun1994.)

⊢ (A ∈ B →
{A} ⊆
B) 

Theorem  snssd 3853 
The singleton of an element of a class is a subset of the class
(deduction rule). (Contributed by Jonathan BenNaim, 3Jun2011.)

⊢ (φ
→ A ∈ B) ⇒ ⊢ (φ
→ {A} ⊆ B) 

Theorem  difsnid 3854 
If we remove a single element from a class then put it back in, we end up
with the original class. (Contributed by NM, 2Oct2006.)

⊢ (B ∈ A →
((A ∖
{B}) ∪ {B}) = A) 

Theorem  pwpw0 3855 
Compute the power set of the power set of the empty set. (See pw0 4160
for
the power set of the empty set.) Theorem 90 of [Suppes] p. 48.
Although this theorem is a special case of pwsn 3881,
we have chosen to
show a direct elementary proof. (Contributed by NM, 7Aug1994.)

⊢ ℘{∅} = {∅,
{∅}} 

Theorem  snsspr1 3856 
A singleton is a subset of an unordered pair containing its member.
(Contributed by NM, 27Aug2004.)

⊢ {A} ⊆ {A,
B} 

Theorem  snsspr2 3857 
A singleton is a subset of an unordered pair containing its member.
(Contributed by NM, 2May2009.)

⊢ {B} ⊆ {A,
B} 

Theorem  snsstp1 3858 
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9Oct2013.)

⊢ {A} ⊆ {A,
B, C} 

Theorem  snsstp2 3859 
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9Oct2013.)

⊢ {B} ⊆ {A,
B, C} 

Theorem  snsstp3 3860 
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9Oct2013.)

⊢ {C} ⊆ {A,
B, C} 

Theorem  prss 3861 
A pair of elements of a class is a subset of the class. Theorem 7.5 of
[Quine] p. 49. (Contributed by NM,
30May1994.) (Proof shortened by
Andrew Salmon, 29Jun2011.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ((A ∈ C ∧ B ∈ C) ↔
{A, B}
⊆ C) 

Theorem  prssg 3862 
A pair of elements of a class is a subset of the class. Theorem 7.5 of
[Quine] p. 49. (Contributed by NM,
22Mar2006.) (Proof shortened by
Andrew Salmon, 29Jun2011.)

⊢ ((A ∈ V ∧ B ∈ W) →
((A ∈
C ∧
B ∈
C) ↔ {A, B} ⊆ C)) 

Theorem  prssi 3863 
A pair of elements of a class is a subset of the class. (Contributed by
NM, 16Jan2015.)

⊢ ((A ∈ C ∧ B ∈ C) →
{A, B}
⊆ C) 

Theorem  sssn 3864 
The subsets of a singleton. (Contributed by NM, 24Apr2004.)

⊢ (A ⊆ {B} ↔
(A = ∅
∨ A =
{B})) 

Theorem  ssunsn2 3865 
The property of being sandwiched between two sets naturally splits under
union with a singleton. This is the induction hypothesis for the
determination of large powersets such as pwtp 3884.
(Contributed by Mario
Carneiro, 2Jul2016.)

⊢ ((B ⊆ A ∧ A ⊆ (C ∪
{D})) ↔ ((B ⊆ A ∧ A ⊆ C) ∨ ((B ∪ {D})
⊆ A
∧ A ⊆ (C ∪
{D})))) 

Theorem  ssunsn 3866 
Possible values for a set sandwiched between another set and it plus a
singleton. (Contributed by Mario Carneiro, 2Jul2016.)

⊢ ((B ⊆ A ∧ A ⊆ (B ∪
{C})) ↔ (A = B ∨ A = (B ∪ {C}))) 

Theorem  eqsn 3867* 
Two ways to express that a nonempty set equals a singleton.
(Contributed by NM, 15Dec2007.)

⊢ (A ≠
∅ → (A = {B} ↔
∀x
∈ A
x = B)) 

Theorem  ssunpr 3868 
Possible values for a set sandwiched between another set and it plus a
singleton. (Contributed by Mario Carneiro, 2Jul2016.)

⊢ ((B ⊆ A ∧ A ⊆ (B ∪
{C, D})) ↔ ((A
= B ∨
A = (B
∪ {C}))
∨ (A = (B ∪ {D})
∨ A =
(B ∪ {C, D})))) 

Theorem  sspr 3869 
The subsets of a pair. (Contributed by NM, 16Mar2006.) (Proof
shortened by Mario Carneiro, 2Jul2016.)

⊢ (A ⊆ {B,
C} ↔ ((A = ∅ ∨ A = {B}) ∨ (A = {C} ∨ A = {B, C}))) 

Theorem  sstp 3870 
The subsets of a triple. (Contributed by Mario Carneiro,
2Jul2016.)

⊢ (A ⊆ {B,
C, D}
↔ (((A = ∅ ∨ A = {B}) ∨ (A =
{C} ∨
A = {B, C})) ∨ ((A =
{D} ∨
A = {B, D}) ∨ (A =
{C, D}
∨ A =
{B, C,
D})))) 

Theorem  tpss 3871 
A triplet of elements of a class is a subset of the class. (Contributed
by NM, 9Apr1994.) (Proof shortened by Andrew Salmon, 29Jun2011.)

⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V ⇒ ⊢ ((A ∈ D ∧ B ∈ D ∧ C ∈ D) ↔
{A, B,
C} ⊆
D) 

Theorem  sneqr 3872 
If the singletons of two sets are equal, the two sets are equal. Part
of Exercise 4 of [TakeutiZaring]
p. 15. (Contributed by NM,
27Aug1993.)

⊢ A ∈ V ⇒ ⊢ ({A} =
{B} → A = B) 

Theorem  snsssn 3873 
If a singleton is a subset of another, their members are equal.
(Contributed by NM, 28May2006.)

⊢ A ∈ V ⇒ ⊢ ({A} ⊆ {B} →
A = B) 

Theorem  sneqrg 3874 
Closed form of sneqr 3872. (Contributed by Scott Fenton, 1Apr2011.)

⊢ (A ∈ V →
({A} = {B} → A =
B)) 

Theorem  sneqbg 3875 
Two singletons of sets are equal iff their elements are equal.
(Contributed by Scott Fenton, 16Apr2012.)

⊢ (A ∈ V →
({A} = {B} ↔ A =
B)) 

Theorem  sneqb 3876 
Biconditional equality for singletons. (Contributed by SF,
14Jan2015.)

⊢ A ∈ V ⇒ ⊢ ({A} =
{B} ↔ A = B) 

Theorem  snsspw 3877 
The singleton of a class is a subset of its power class. (Contributed
by NM, 5Aug1993.)

⊢ {A} ⊆ ℘A 

Theorem  prsspw 3878 
An unordered pair belongs to the power class of a class iff each member
belongs to the class. (Contributed by NM, 10Dec2003.) (Proof
shortened by Andrew Salmon, 26Jun2011.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ({A,
B} ⊆
℘C
↔ (A ⊆ C ∧ B ⊆ C)) 

Theorem  ralunsn 3879* 
Restricted quantification over the union of a set and a singleton, using
implicit substitution. (Contributed by Paul Chapman, 17Nov2012.)
(Revised by Mario Carneiro, 23Apr2015.)

⊢ (x =
B → (φ ↔ ψ)) ⇒ ⊢ (B ∈ C →
(∀x
∈ (A
∪ {B})φ ↔ (∀x ∈ A φ ∧ ψ))) 

Theorem  2ralunsn 3880* 
Double restricted quantification over the union of a set and a
singleton, using implicit substitution. (Contributed by Paul Chapman,
17Nov2012.)

⊢ (x =
B → (φ ↔ χ))
& ⊢ (y =
B → (φ ↔ ψ))
& ⊢ (x =
B → (ψ ↔ θ)) ⇒ ⊢ (B ∈ C →
(∀x
∈ (A
∪ {B})∀y ∈ (A ∪
{B})φ ↔ ((∀x ∈ A ∀y ∈ A φ ∧ ∀x ∈ A ψ) ∧ (∀y ∈ A χ ∧ θ)))) 

Theorem  pwsn 3881 
The power set of a singleton. (Contributed by NM, 5Jun2006.)

⊢ ℘{A} = {∅,
{A}} 

Theorem  pwsnALT 3882 
The power set of a singleton (direct proof). TO DO  should we keep
this? (Contributed by NM, 5Jun2006.)
(Proof modification is discouraged.) (New usage is discouraged.)

⊢ ℘{A} = {∅,
{A}} 

Theorem  pwpr 3883 
The power set of an unordered pair. (Contributed by NM, 1May2009.)

⊢ ℘{A, B} = ({∅, {A}} ∪
{{B}, {A, B}}) 

Theorem  pwtp 3884 
The power set of an unordered triple. (Contributed by Mario Carneiro,
2Jul2016.)

⊢ ℘{A, B, C} = (({∅,
{A}} ∪ {{B}, {A,
B}}) ∪ ({{C}, {A,
C}} ∪ {{B, C},
{A, B,
C}})) 

Theorem  pwpwpw0 3885 
Compute the power set of the power set of the power set of the empty
set. (See also pw0 4160 and pwpw0 3855.) (Contributed by NM,
2May2009.)

⊢ ℘{∅, {∅}} =
({∅, {∅}} ∪ {{{∅}}, {∅,
{∅}}}) 

Theorem  pwv 3886 
The power class of the universe is the universe. Exercise 4.12(d) of
[Mendelson] p. 235. (Contributed by
NM, 14Sep2003.)

⊢ ℘V =
V 

Theorem  unsneqsn 3887 
If union with a singleton yields a singleton, then the first argument is
either also the singleton or is the empty set. (Contributed by SF,
15Jan2015.)

⊢ B ∈ V ⇒ ⊢ ((A ∪
{B}) = {C} → (A =
∅ ∨
A = {B})) 

Theorem  dfpss4 3888* 
Alternate definition of proper subset. Theorem IX.4.21 of [Rosser]
p. 236. (Contributed by SF, 19Jan2015.)

⊢ (A ⊂ B ↔
(A ⊆
B ∧ ∃x ∈ B ¬
x ∈
A)) 

Theorem  adj11 3889 
Adjoining a new element is onetoone. (Contributed by SF,
29Jan2015.)

⊢ ((¬ C
∈ A
∧ ¬ C
∈ B)
→ ((A ∪ {C}) = (B ∪
{C}) ↔ A = B)) 

Theorem  disj5 3890 
Two ways of saying that two classes are disjoint. (Contributed by SF,
5Feb2015.)

⊢ ((A ∩
B) = ∅
↔ A ⊆ ∼ B) 

2.1.17 The union of a class


Syntax  cuni 3891 
Extend class notation to include the union of a class (read: 'union
A')

class
∪A 

Definition  dfuni 3892* 
Define the union of a class i.e. the collection of all members of the
members of the class. Definition 5.5 of [TakeutiZaring] p. 16. For
example, ∪{{1, 3}, {1, 8}} = {1, 3,
8} (exuni (future)).
This is similar to the union of two classes dfun 3214. (Contributed by
NM, 23Aug1993.)

⊢ ∪A = {x ∣ ∃y(x ∈ y ∧ y ∈ A)} 

Theorem  dfuni2 3893* 
Alternate definition of class union. (Contributed by NM,
28Jun1998.)

⊢ ∪A = {x ∣ ∃y ∈ A x ∈ y} 

Theorem  eluni 3894* 
Membership in class union. (Contributed by NM, 22May1994.)

⊢ (A ∈ ∪B ↔ ∃x(A ∈ x ∧ x ∈ B)) 

Theorem  eluni2 3895* 
Membership in class union. Restricted quantifier version. (Contributed
by NM, 31Aug1999.)

⊢ (A ∈ ∪B ↔ ∃x ∈ B A ∈ x) 

Theorem  elunii 3896 
Membership in class union. (Contributed by NM, 24Mar1995.)

⊢ ((A ∈ B ∧ B ∈ C) →
A ∈
∪C) 

Theorem  nfuni 3897 
Boundvariable hypothesis builder for union. (Contributed by NM,
30Dec1996.) (Proof shortened by Andrew Salmon, 27Aug2011.)

⊢ F/_xA ⇒ ⊢ F/_x∪A 

Theorem  nfunid 3898 
Deduction version of nfuni 3897. (Contributed by NM, 18Feb2013.)

⊢ (φ
→ F/_xA) ⇒ ⊢ (φ
→ F/_x∪A) 

Theorem  csbunig 3899 
Distribute proper substitution through the union of a class.
(Contributed by Alan Sare, 10Nov2012.)

⊢ (A ∈ V →
[A / x]∪B = ∪[A / x]B) 

Theorem  unieq 3900 
Equality theorem for class union. Exercise 15 of [TakeutiZaring]
p. 18. (Contributed by NM, 10Aug1993.) (Proof shortened by Andrew
Salmon, 29Jun2011.)

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