Type  Label  Description 
Statement 

Theorem  difsn 3501 
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 3502 
Removal of a singleton from an unordered pair. (Contributed by NM,
16Mar2006.) (Proof shortened by Andrew Salmon, 29Jun2011.)



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



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



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



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



Theorem  difsnpssim 3507 
is a proper subclass of if is a member of
. In classical
logic, the converse holds as well. (Contributed by
Jim Kingdon, 9Aug2018.)



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



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



Theorem  difsnss 3510 
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 6080. (Contributed by Jim
Kingdon, 10Aug2018.)



Theorem  pw0 3511 
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 3512 
A singleton is a subset of an unordered pair containing its member.
(Contributed by NM, 27Aug2004.)



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



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



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



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



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



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



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



Theorem  prss 3520 
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 3521 
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 3522 
A pair of elements of a class is a subset of the class. (Contributed by
NM, 16Jan2015.)



Theorem  prsspwg 3523 
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 3524 
Empty set and the singleton itself are subsets of a singleton.
(Contributed by Jim Kingdon, 10Aug2018.)



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



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



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



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



Theorem  tpss 3529 
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 3530 
A triple of elements of a class is a subset of the class. (Contributed by
Alexander van der Vekens, 1Feb2018.)



Theorem  sneqr 3531 
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 3532 
If a singleton is a subset of another, their members are equal.
(Contributed by NM, 28May2006.)



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



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



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



Theorem  prsspw 3536 
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 3537 
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same second element, the first elements are equal. Closed form of
preqr1 3539. (Contributed by Jim Kingdon, 21Sep2018.)



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



Theorem  preqr1 3539 
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 3540 
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 3541 
Equality relationship for two unordered pairs. (Contributed by NM,
17Oct1996.)



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



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



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



Theorem  prneimg 3545 
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 3546 
Equivalence for a pair equal to a singleton. (Contributed by NM,
3Jun2008.)



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



Theorem  dfop 3548 
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 3549 
Equality theorem for ordered pairs. (Contributed by NM, 25Jun1998.)
(Revised by Mario Carneiro, 26Apr2015.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  ralunsn 3568* 
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 3569* 
Double restricted quantification over the union of a set and a
singleton, using implicit substitution. (Contributed by Paul Chapman,
17Nov2012.)



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



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



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



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



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



Theorem  pwpw0ss 3575 
Compute the power set of the power set of the empty set. (See pw0 3511
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 3576 
The power set of an unordered pair. (Contributed by Jim Kingdon,
13Aug2018.)



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



Theorem  pwpwpw0ss 3578 
Compute the power set of the power set of the power set of the empty
set. (See also pw0 3511 and pwpw0ss 3575.) (Contributed by Jim Kingdon,
13Aug2018.)



Theorem  pwv 3579 
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 3580 
Extend class notation to include the union of a class (read: 'union
')



Definition  dfuni 3581* 
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 2922. (Contributed by NM, 23Aug1993.)



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



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



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



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



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



Theorem  nfunid 3587 
Deduction version of nfuni 3586. (Contributed by NM, 18Feb2013.)



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



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



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



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



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



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



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



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



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



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



Theorem  dfnfc2 3598* 
An alternative statement of the effective freeness of a class ,
when it is a set. (Contributed by Mario Carneiro, 14Oct2016.)



Theorem  uniun 3599 
The class union of the union of two classes. Theorem 8.3 of [Quine]
p. 53. (Contributed by NM, 20Aug1993.)



Theorem  uniin 3600 
The class union of the intersection of two classes. Exercise 4.12(n) of
[Mendelson] p. 235. (Contributed by
NM, 4Dec2003.) (Proof shortened
by Andrew Salmon, 29Jun2011.)

