Theorem List for Intuitionistic Logic Explorer - 3501-3600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | prprc2 3501 |
A proper class vanishes in an unordered pair. (Contributed by NM,
22-Mar-2006.)
|
|
|
Theorem | prprc 3502 |
An unordered pair containing two proper classes is the empty set.
(Contributed by NM, 22-Mar-2006.)
|
|
|
Theorem | tpid1 3503 |
One of the three elements of an unordered triple. (Contributed by NM,
7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | tpid2 3504 |
One of the three elements of an unordered triple. (Contributed by NM,
7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | tpid3g 3505 |
Closed theorem form of tpid3 3506. (Contributed by Alan Sare,
24-Oct-2011.)
|
|
|
Theorem | tpid3 3506 |
One of the three elements of an unordered triple. (Contributed by NM,
7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | snnzg 3507 |
The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
|
|
|
Theorem | snmg 3508* |
The singleton of a set is inhabited. (Contributed by Jim Kingdon,
11-Aug-2018.)
|
|
|
Theorem | snnz 3509 |
The singleton of a set is not empty. (Contributed by NM,
10-Apr-1994.)
|
|
|
Theorem | snm 3510* |
The singleton of a set is inhabited. (Contributed by Jim Kingdon,
11-Aug-2018.)
|
|
|
Theorem | prmg 3511* |
A pair containing a set is inhabited. (Contributed by Jim Kingdon,
21-Sep-2018.)
|
|
|
Theorem | prnz 3512 |
A pair containing a set is not empty. (Contributed by NM,
9-Apr-1994.)
|
|
|
Theorem | prm 3513* |
A pair containing a set is inhabited. (Contributed by Jim Kingdon,
21-Sep-2018.)
|
|
|
Theorem | prnzg 3514 |
A pair containing a set is not empty. (Contributed by FL,
19-Sep-2011.)
|
|
|
Theorem | tpnz 3515 |
A triplet containing a set is not empty. (Contributed by NM,
10-Apr-1994.)
|
|
|
Theorem | snss 3516 |
The singleton of an element of a class is a subset of the class.
Theorem 7.4 of [Quine] p. 49.
(Contributed by NM, 5-Aug-1993.)
|
|
|
Theorem | eldifsn 3517 |
Membership in a set with an element removed. (Contributed by NM,
10-Oct-2007.)
|
|
|
Theorem | eldifsni 3518 |
Membership in a set with an element removed. (Contributed by NM,
10-Mar-2015.)
|
|
|
Theorem | neldifsn 3519 |
is not in . (Contributed by David Moews,
1-May-2017.)
|
|
|
Theorem | neldifsnd 3520 |
is not in . Deduction form. (Contributed by
David Moews, 1-May-2017.)
|
|
|
Theorem | rexdifsn 3521 |
Restricted existential quantification over a set with an element removed.
(Contributed by NM, 4-Feb-2015.)
|
|
|
Theorem | snssg 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, 22-Jul-2001.)
|
|
|
Theorem | difsn 3523 |
An element not in a set can be removed without affecting the set.
(Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
|
|
Theorem | difprsnss 3524 |
Removal of a singleton from an unordered pair. (Contributed by NM,
16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | difprsn1 3525 |
Removal of a singleton from an unordered pair. (Contributed by Thierry
Arnoux, 4-Feb-2017.)
|
|
|
Theorem | difprsn2 3526 |
Removal of a singleton from an unordered pair. (Contributed by Alexander
van der Vekens, 5-Oct-2017.)
|
|
|
Theorem | diftpsn3 3527 |
Removal of a singleton from an unordered triple. (Contributed by
Alexander van der Vekens, 5-Oct-2017.)
|
|
|
Theorem | difsnb 3528 |
equals if and only if is not a member of
. Generalization
of difsn 3523. (Contributed by David Moews,
1-May-2017.)
|
|
|
Theorem | snssi 3529 |
The singleton of an element of a class is a subset of the class.
(Contributed by NM, 6-Jun-1994.)
|
|
|
Theorem | snssd 3530 |
The singleton of an element of a class is a subset of the class
(deduction rule). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|
|
|
Theorem | difsnss 3531 |
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 6103. (Contributed by Jim
Kingdon, 10-Aug-2018.)
|
|
|
Theorem | pw0 3532 |
Compute the power set of the empty set. Theorem 89 of [Suppes] p. 47.
(Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
|
|
Theorem | snsspr1 3533 |
A singleton is a subset of an unordered pair containing its member.
(Contributed by NM, 27-Aug-2004.)
|
|
|
Theorem | snsspr2 3534 |
A singleton is a subset of an unordered pair containing its member.
(Contributed by NM, 2-May-2009.)
|
|
|
Theorem | snsstp1 3535 |
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9-Oct-2013.)
|
|
|
Theorem | snsstp2 3536 |
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9-Oct-2013.)
|
|
|
Theorem | snsstp3 3537 |
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9-Oct-2013.)
|
|
|
Theorem | prsstp12 3538 |
A pair is a subset of an unordered triple containing its members.
(Contributed by Jim Kingdon, 11-Aug-2018.)
|
|
|
Theorem | prsstp13 3539 |
A pair is a subset of an unordered triple containing its members.
(Contributed by Jim Kingdon, 11-Aug-2018.)
|
|
|
Theorem | prsstp23 3540 |
A pair is a subset of an unordered triple containing its members.
(Contributed by Jim Kingdon, 11-Aug-2018.)
|
|
|
Theorem | prss 3541 |
A pair of elements of a class is a subset of the class. Theorem 7.5 of
[Quine] p. 49. (Contributed by NM,
30-May-1994.) (Proof shortened by
Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | prssg 3542 |
A pair of elements of a class is a subset of the class. Theorem 7.5 of
[Quine] p. 49. (Contributed by NM,
22-Mar-2006.) (Proof shortened by
Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | prssi 3543 |
A pair of elements of a class is a subset of the class. (Contributed by
NM, 16-Jan-2015.)
|
|
|
Theorem | prsspwg 3544 |
An unordered pair belongs to the power class of a class iff each member
belongs to the class. (Contributed by Thierry Arnoux, 3-Oct-2016.)
(Revised by NM, 18-Jan-2018.)
|
|
|
Theorem | sssnr 3545 |
Empty set and the singleton itself are subsets of a singleton.
(Contributed by Jim Kingdon, 10-Aug-2018.)
|
|
|
Theorem | sssnm 3546* |
The inhabited subset of a singleton. (Contributed by Jim Kingdon,
10-Aug-2018.)
|
|
|
Theorem | eqsnm 3547* |
Two ways to express that an inhabited set equals a singleton.
(Contributed by Jim Kingdon, 11-Aug-2018.)
|
|
|
Theorem | ssprr 3548 |
The subsets of a pair. (Contributed by Jim Kingdon, 11-Aug-2018.)
|
|
|
Theorem | sstpr 3549 |
The subsets of a triple. (Contributed by Jim Kingdon, 11-Aug-2018.)
|
|
|
Theorem | tpss 3550 |
A triplet of elements of a class is a subset of the class. (Contributed
by NM, 9-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | tpssi 3551 |
A triple of elements of a class is a subset of the class. (Contributed by
Alexander van der Vekens, 1-Feb-2018.)
|
|
|
Theorem | sneqr 3552 |
If the singletons of two sets are equal, the two sets are equal. Part
of Exercise 4 of [TakeutiZaring]
p. 15. (Contributed by NM,
27-Aug-1993.)
|
|
|
Theorem | snsssn 3553 |
If a singleton is a subset of another, their members are equal.
(Contributed by NM, 28-May-2006.)
|
|
|
Theorem | sneqrg 3554 |
Closed form of sneqr 3552. (Contributed by Scott Fenton, 1-Apr-2011.)
|
|
|
Theorem | sneqbg 3555 |
Two singletons of sets are equal iff their elements are equal.
(Contributed by Scott Fenton, 16-Apr-2012.)
|
|
|
Theorem | snsspw 3556 |
The singleton of a class is a subset of its power class. (Contributed
by NM, 5-Aug-1993.)
|
|
|
Theorem | prsspw 3557 |
An unordered pair belongs to the power class of a class iff each member
belongs to the class. (Contributed by NM, 10-Dec-2003.) (Proof
shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | preqr1g 3558 |
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same second element, the first elements are equal. Closed form of
preqr1 3560. (Contributed by Jim Kingdon, 21-Sep-2018.)
|
|
|
Theorem | preqr2g 3559 |
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same second element, the second elements are equal. Closed form of
preqr2 3561. (Contributed by Jim Kingdon, 21-Sep-2018.)
|
|
|
Theorem | preqr1 3560 |
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same second element, the first elements are equal. (Contributed by
NM, 18-Oct-1995.)
|
|
|
Theorem | preqr2 3561 |
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same first element, the second elements are equal. (Contributed by
NM, 5-Aug-1993.)
|
|
|
Theorem | preq12b 3562 |
Equality relationship for two unordered pairs. (Contributed by NM,
17-Oct-1996.)
|
|
|
Theorem | prel12 3563 |
Equality of two unordered pairs. (Contributed by NM, 17-Oct-1996.)
|
|
|
Theorem | opthpr 3564 |
A way to represent ordered pairs using unordered pairs with distinct
members. (Contributed by NM, 27-Mar-2007.)
|
|
|
Theorem | preq12bg 3565 |
Closed form of preq12b 3562. (Contributed by Scott Fenton,
28-Mar-2014.)
|
|
|
Theorem | prneimg 3566 |
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,
13-Aug-2017.)
|
|
|
Theorem | preqsn 3567 |
Equivalence for a pair equal to a singleton. (Contributed by NM,
3-Jun-2008.)
|
|
|
Theorem | dfopg 3568 |
Value of the ordered pair when the arguments are sets. (Contributed by
Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | dfop 3569 |
Value of an ordered pair when the arguments are sets, with the
conclusion corresponding to Kuratowski's original definition.
(Contributed by NM, 25-Jun-1998.)
|
|
|
Theorem | opeq1 3570 |
Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.)
(Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | opeq2 3571 |
Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.)
(Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | opeq12 3572 |
Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)
|
|
|
Theorem | opeq1i 3573 |
Equality inference for ordered pairs. (Contributed by NM,
16-Dec-2006.)
|
|
|
Theorem | opeq2i 3574 |
Equality inference for ordered pairs. (Contributed by NM,
16-Dec-2006.)
|
|
|
Theorem | opeq12i 3575 |
Equality inference for ordered pairs. (Contributed by NM,
16-Dec-2006.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|
|
|
Theorem | opeq1d 3576 |
Equality deduction for ordered pairs. (Contributed by NM,
16-Dec-2006.)
|
|
|
Theorem | opeq2d 3577 |
Equality deduction for ordered pairs. (Contributed by NM,
16-Dec-2006.)
|
|
|
Theorem | opeq12d 3578 |
Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
(Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | oteq1 3579 |
Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|
|
|
Theorem | oteq2 3580 |
Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|
|
|
Theorem | oteq3 3581 |
Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|
|
|
Theorem | oteq1d 3582 |
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11-Jan-2017.)
|
|
|
Theorem | oteq2d 3583 |
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11-Jan-2017.)
|
|
|
Theorem | oteq3d 3584 |
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11-Jan-2017.)
|
|
|
Theorem | oteq123d 3585 |
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11-Jan-2017.)
|
|
|
Theorem | nfop 3586 |
Bound-variable hypothesis builder for ordered pairs. (Contributed by
NM, 14-Nov-1995.)
|
|
|
Theorem | nfopd 3587 |
Deduction version of bound-variable hypothesis builder nfop 3586.
This
shows how the deduction version of a not-free theorem such as nfop 3586
can
be created from the corresponding not-free inference theorem.
(Contributed by NM, 4-Feb-2008.)
|
|
|
Theorem | opid 3588 |
The ordered pair in Kuratowski's representation.
(Contributed by FL, 28-Dec-2011.)
|
|
|
Theorem | ralunsn 3589* |
Restricted quantification over the union of a set and a singleton, using
implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.)
(Revised by Mario Carneiro, 23-Apr-2015.)
|
|
|
Theorem | 2ralunsn 3590* |
Double restricted quantification over the union of a set and a
singleton, using implicit substitution. (Contributed by Paul Chapman,
17-Nov-2012.)
|
|
|
Theorem | opprc 3591 |
Expansion of an ordered pair when either member is a proper class.
(Contributed by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | opprc1 3592 |
Expansion of an ordered pair when the first member is a proper class. See
also opprc 3591. (Contributed by NM, 10-Apr-2004.) (Revised
by Mario
Carneiro, 26-Apr-2015.)
|
|
|
Theorem | opprc2 3593 |
Expansion of an ordered pair when the second member is a proper class.
See also opprc 3591. (Contributed by NM, 15-Nov-1994.) (Revised
by Mario
Carneiro, 26-Apr-2015.)
|
|
|
Theorem | oprcl 3594 |
If an ordered pair has an element, then its arguments are sets.
(Contributed by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | pwsnss 3595 |
The power set of a singleton. (Contributed by Jim Kingdon,
12-Aug-2018.)
|
|
|
Theorem | pwpw0ss 3596 |
Compute the power set of the power set of the empty set. (See pw0 3532
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,
12-Aug-2018.)
|
|
|
Theorem | pwprss 3597 |
The power set of an unordered pair. (Contributed by Jim Kingdon,
13-Aug-2018.)
|
|
|
Theorem | pwtpss 3598 |
The power set of an unordered triple. (Contributed by Jim Kingdon,
13-Aug-2018.)
|
|
|
Theorem | pwpwpw0ss 3599 |
Compute the power set of the power set of the power set of the empty set.
(See also pw0 3532 and pwpw0ss 3596.) (Contributed by Jim Kingdon,
13-Aug-2018.)
|
|
|
Theorem | pwv 3600 |
The power class of the universe is the universe. Exercise 4.12(d) of
[Mendelson] p. 235. (Contributed by NM,
14-Sep-2003.)
|
|