Type  Label  Description 
Statement 

Theorem  tppreq3 3501 
An unordered triple is an unordered pair if one of its elements is
identical with another element. (Contributed by Alexander van der Vekens,
6Oct2017.)



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



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



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



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



Theorem  prprc1 3506 
A proper class vanishes in an unordered pair. (Contributed by NM,
5Aug1993.)



Theorem  prprc2 3507 
A proper class vanishes in an unordered pair. (Contributed by NM,
22Mar2006.)



Theorem  prprc 3508 
An unordered pair containing two proper classes is the empty set.
(Contributed by NM, 22Mar2006.)



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



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



Theorem  tpid3g 3511 
Closed theorem form of tpid3 3512. (Contributed by Alan Sare,
24Oct2011.)



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



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



Theorem  snmg 3514* 
The singleton of a set is inhabited. (Contributed by Jim Kingdon,
11Aug2018.)



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



Theorem  snm 3516* 
The singleton of a set is inhabited. (Contributed by Jim Kingdon,
11Aug2018.)



Theorem  prmg 3517* 
A pair containing a set is inhabited. (Contributed by Jim Kingdon,
21Sep2018.)



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



Theorem  prm 3519* 
A pair containing a set is inhabited. (Contributed by Jim Kingdon,
21Sep2018.)



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



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



Theorem  snss 3522 
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.)



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



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



Theorem  neldifsn 3525 
is not in . (Contributed by David Moews,
1May2017.)



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



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



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



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



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



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



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



Theorem  difsnpssim 3535 
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 3536 
The singleton of an element of a class is a subset of the class.
(Contributed by NM, 6Jun1994.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

