Type  Label  Description 
Statement 

Theorem  difsnss 3501 
If we remove a single element from a class then put it back in, we end up
with a subset of the original class. In classical logic, we could replace
subset with equality. (Contributed by Jim Kingdon, 10Aug2018.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  pwpwpw0ss 3569 
Compute the power set of the power set of the power set of the empty
set. (See also pw0 3502 and pwpw0ss 3566.) (Contributed by Jim Kingdon,
13Aug2018.)



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



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



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



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



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



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



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



Theorem  nfunid 3578 
Deduction version of nfuni 3577. (Contributed by NM, 18Feb2013.)



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  uniin 3591 
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.)



Theorem  uniss 3592 
Subclass relationship for class union. Theorem 61 of [Suppes] p. 39.
(Contributed by NM, 22Mar1998.) (Proof shortened by Andrew Salmon,
29Jun2011.)



Theorem  ssuni 3593 
Subclass relationship for class union. (Contributed by NM,
24May1994.) (Proof shortened by Andrew Salmon, 29Jun2011.)



Theorem  unissi 3594 
Subclass relationship for subclass union. Inference form of uniss 3592.
(Contributed by David Moews, 1May2017.)



Theorem  unissd 3595 
Subclass relationship for subclass union. Deduction form of uniss 3592.
(Contributed by David Moews, 1May2017.)



Theorem  uni0b 3596 
The union of a set is empty iff the set is included in the singleton of
the empty set. (Contributed by NM, 12Sep2004.)



Theorem  uni0c 3597* 
The union of a set is empty iff all of its members are empty.
(Contributed by NM, 16Aug2006.)



Theorem  uni0 3598 
The union of the empty set is the empty set. Theorem 8.7 of [Quine]
p. 54. (Reproved without relying on axnul by Eric Schmidt.)
(Contributed by NM, 16Sep1993.) (Revised by Eric Schmidt,
4Apr2007.)



Theorem  elssuni 3599 
An element of a class is a subclass of its union. Theorem 8.6 of [Quine]
p. 54. Also the basis for Proposition 7.20 of [TakeutiZaring] p. 40.
(Contributed by NM, 6Jun1994.)



Theorem  unissel 3600 
Condition turning a subclass relationship for union into an equality.
(Contributed by NM, 18Jul2006.)

