Type  Label  Description 
Statement 

Theorem  neldifsnd 3601 
is not in . Deduction form. (Contributed by
David Moews, 1May2017.)



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



Theorem  snssg 3603 
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.)



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



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



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



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



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



Theorem  difpr 3609 
Removing two elements as pair of elements corresponds to removing each of
the two elements as singletons. (Contributed by Alexander van der Vekens,
13Jul2018.)



Theorem  difsnb 3610 
equals if and only if is not a member of
. Generalization
of difsn 3604. (Contributed by David Moews,
1May2017.)



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



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



Theorem  difsnss 3613 
If we remove a single element from a class then put it back in, we end up
with a subset of the original class. If equality is decidable, we can
replace subset with equality as seen in nndifsnid 6333. (Contributed by Jim
Kingdon, 10Aug2018.)



Theorem  pw0 3614 
Compute the power set of the empty set. Theorem 89 of [Suppes] p. 47.
(Contributed by NM, 5Aug1993.) (Proof shortened by Andrew Salmon,
29Jun2011.)



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



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



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



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



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



Theorem  prsstp12 3620 
A pair is a subset of an unordered triple containing its members.
(Contributed by Jim Kingdon, 11Aug2018.)



Theorem  prsstp13 3621 
A pair is a subset of an unordered triple containing its members.
(Contributed by Jim Kingdon, 11Aug2018.)



Theorem  prsstp23 3622 
A pair is a subset of an unordered triple containing its members.
(Contributed by Jim Kingdon, 11Aug2018.)



Theorem  prss 3623 
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.)



Theorem  prssg 3624 
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.)



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



Theorem  prsspwg 3626 
An unordered pair belongs to the power class of a class iff each member
belongs to the class. (Contributed by Thierry Arnoux, 3Oct2016.)
(Revised by NM, 18Jan2018.)



Theorem  sssnr 3627 
Empty set and the singleton itself are subsets of a singleton.
Concerning the converse, see exmidsssn 4063. (Contributed by Jim Kingdon,
10Aug2018.)



Theorem  sssnm 3628* 
The inhabited subset of a singleton. (Contributed by Jim Kingdon,
10Aug2018.)



Theorem  eqsnm 3629* 
Two ways to express that an inhabited set equals a singleton.
(Contributed by Jim Kingdon, 11Aug2018.)



Theorem  ssprr 3630 
The subsets of a pair. (Contributed by Jim Kingdon, 11Aug2018.)



Theorem  sstpr 3631 
The subsets of a triple. (Contributed by Jim Kingdon, 11Aug2018.)



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



Theorem  tpssi 3633 
A triple of elements of a class is a subset of the class. (Contributed by
Alexander van der Vekens, 1Feb2018.)



Theorem  sneqr 3634 
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.)



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



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



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



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



Theorem  prsspw 3639 
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.)



Theorem  preqr1g 3640 
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same second element, the first elements are equal. Closed form of
preqr1 3642. (Contributed by Jim Kingdon, 21Sep2018.)



Theorem  preqr2g 3641 
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same second element, the second elements are equal. Closed form of
preqr2 3643. (Contributed by Jim Kingdon, 21Sep2018.)



Theorem  preqr1 3642 
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same second element, the first elements are equal. (Contributed by
NM, 18Oct1995.)



Theorem  preqr2 3643 
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same first element, the second elements are equal. (Contributed by
NM, 5Aug1993.)



Theorem  preq12b 3644 
Equality relationship for two unordered pairs. (Contributed by NM,
17Oct1996.)



Theorem  prel12 3645 
Equality of two unordered pairs. (Contributed by NM, 17Oct1996.)



Theorem  opthpr 3646 
A way to represent ordered pairs using unordered pairs with distinct
members. (Contributed by NM, 27Mar2007.)



Theorem  preq12bg 3647 
Closed form of preq12b 3644. (Contributed by Scott Fenton,
28Mar2014.)



Theorem  prneimg 3648 
Two pairs are not equal if at least one element of the first pair is not
contained in the second pair. (Contributed by Alexander van der Vekens,
13Aug2017.)



Theorem  preqsn 3649 
Equivalence for a pair equal to a singleton. (Contributed by NM,
3Jun2008.)



Theorem  dfopg 3650 
Value of the ordered pair when the arguments are sets. (Contributed by
Mario Carneiro, 26Apr2015.)



Theorem  dfop 3651 
Value of an ordered pair when the arguments are sets, with the
conclusion corresponding to Kuratowski's original definition.
(Contributed by NM, 25Jun1998.)



Theorem  opeq1 3652 
Equality theorem for ordered pairs. (Contributed by NM, 25Jun1998.)
(Revised by Mario Carneiro, 26Apr2015.)



Theorem  opeq2 3653 
Equality theorem for ordered pairs. (Contributed by NM, 25Jun1998.)
(Revised by Mario Carneiro, 26Apr2015.)



Theorem  opeq12 3654 
Equality theorem for ordered pairs. (Contributed by NM, 28May1995.)



Theorem  opeq1i 3655 
Equality inference for ordered pairs. (Contributed by NM,
16Dec2006.)



Theorem  opeq2i 3656 
Equality inference for ordered pairs. (Contributed by NM,
16Dec2006.)



Theorem  opeq12i 3657 
Equality inference for ordered pairs. (Contributed by NM,
16Dec2006.) (Proof shortened by Eric Schmidt, 4Apr2007.)



Theorem  opeq1d 3658 
Equality deduction for ordered pairs. (Contributed by NM,
16Dec2006.)



Theorem  opeq2d 3659 
Equality deduction for ordered pairs. (Contributed by NM,
16Dec2006.)



Theorem  opeq12d 3660 
Equality deduction for ordered pairs. (Contributed by NM, 16Dec2006.)
(Proof shortened by Andrew Salmon, 29Jun2011.)



Theorem  oteq1 3661 
Equality theorem for ordered triples. (Contributed by NM, 3Apr2015.)



Theorem  oteq2 3662 
Equality theorem for ordered triples. (Contributed by NM, 3Apr2015.)



Theorem  oteq3 3663 
Equality theorem for ordered triples. (Contributed by NM, 3Apr2015.)



Theorem  oteq1d 3664 
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11Jan2017.)



Theorem  oteq2d 3665 
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11Jan2017.)



Theorem  oteq3d 3666 
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11Jan2017.)



Theorem  oteq123d 3667 
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11Jan2017.)



Theorem  nfop 3668 
Boundvariable hypothesis builder for ordered pairs. (Contributed by
NM, 14Nov1995.)



Theorem  nfopd 3669 
Deduction version of boundvariable hypothesis builder nfop 3668.
This
shows how the deduction version of a notfree theorem such as nfop 3668
can
be created from the corresponding notfree inference theorem.
(Contributed by NM, 4Feb2008.)



Theorem  opid 3670 
The ordered pair in Kuratowski's representation.
(Contributed by FL, 28Dec2011.)



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



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



Theorem  opprc 3673 
Expansion of an ordered pair when either member is a proper class.
(Contributed by Mario Carneiro, 26Apr2015.)



Theorem  opprc1 3674 
Expansion of an ordered pair when the first member is a proper class. See
also opprc 3673. (Contributed by NM, 10Apr2004.) (Revised
by Mario
Carneiro, 26Apr2015.)



Theorem  opprc2 3675 
Expansion of an ordered pair when the second member is a proper class.
See also opprc 3673. (Contributed by NM, 15Nov1994.) (Revised
by Mario
Carneiro, 26Apr2015.)



Theorem  oprcl 3676 
If an ordered pair has an element, then its arguments are sets.
(Contributed by Mario Carneiro, 26Apr2015.)



Theorem  pwsnss 3677 
The power set of a singleton. (Contributed by Jim Kingdon,
12Aug2018.)



Theorem  pwpw0ss 3678 
Compute the power set of the power set of the empty set. (See pw0 3614
for
the power set of the empty set.) Theorem 90 of [Suppes] p. 48 (but with
subset in place of equality). (Contributed by Jim Kingdon,
12Aug2018.)



Theorem  pwprss 3679 
The power set of an unordered pair. (Contributed by Jim Kingdon,
13Aug2018.)



Theorem  pwtpss 3680 
The power set of an unordered triple. (Contributed by Jim Kingdon,
13Aug2018.)



Theorem  pwpwpw0ss 3681 
Compute the power set of the power set of the power set of the empty set.
(See also pw0 3614 and pwpw0ss 3678.) (Contributed by Jim Kingdon,
13Aug2018.)



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



2.1.18 The union of a class


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



Definition  dfuni 3684* 
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 } . This is similar to
the union of two classes dfun 3025. (Contributed by NM, 23Aug1993.)



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



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



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



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



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



Theorem  nfunid 3690 
Deduction version of nfuni 3689. (Contributed by NM, 18Feb2013.)



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



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



Theorem  unieqi 3693 
Inference of equality of two class unions. (Contributed by NM,
30Aug1993.)



Theorem  unieqd 3694 
Deduction of equality of two class unions. (Contributed by NM,
21Apr1995.)



Theorem  eluniab 3695* 
Membership in union of a class abstraction. (Contributed by NM,
11Aug1994.) (Revised by Mario Carneiro, 14Nov2016.)



Theorem  elunirab 3696* 
Membership in union of a class abstraction. (Contributed by NM,
4Oct2006.)



Theorem  unipr 3697 
The union of a pair is the union of its members. Proposition 5.7 of
[TakeutiZaring] p. 16.
(Contributed by NM, 23Aug1993.)



Theorem  uniprg 3698 
The union of a pair is the union of its members. Proposition 5.7 of
[TakeutiZaring] p. 16.
(Contributed by NM, 25Aug2006.)



Theorem  unisn 3699 
A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
(Contributed by NM, 30Aug1993.)



Theorem  unisng 3700 
A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
(Contributed by NM, 13Aug2002.)

