Theorem List for Intuitionistic Logic Explorer - 3701-3800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | opeq2 3701 |
Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.)
(Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | opeq12 3702 |
Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)
|
|
|
Theorem | opeq1i 3703 |
Equality inference for ordered pairs. (Contributed by NM,
16-Dec-2006.)
|
|
|
Theorem | opeq2i 3704 |
Equality inference for ordered pairs. (Contributed by NM,
16-Dec-2006.)
|
|
|
Theorem | opeq12i 3705 |
Equality inference for ordered pairs. (Contributed by NM,
16-Dec-2006.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|
|
|
Theorem | opeq1d 3706 |
Equality deduction for ordered pairs. (Contributed by NM,
16-Dec-2006.)
|
|
|
Theorem | opeq2d 3707 |
Equality deduction for ordered pairs. (Contributed by NM,
16-Dec-2006.)
|
|
|
Theorem | opeq12d 3708 |
Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
(Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | oteq1 3709 |
Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|
|
|
Theorem | oteq2 3710 |
Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|
|
|
Theorem | oteq3 3711 |
Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|
|
|
Theorem | oteq1d 3712 |
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11-Jan-2017.)
|
|
|
Theorem | oteq2d 3713 |
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11-Jan-2017.)
|
|
|
Theorem | oteq3d 3714 |
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11-Jan-2017.)
|
|
|
Theorem | oteq123d 3715 |
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11-Jan-2017.)
|
|
|
Theorem | nfop 3716 |
Bound-variable hypothesis builder for ordered pairs. (Contributed by
NM, 14-Nov-1995.)
|
|
|
Theorem | nfopd 3717 |
Deduction version of bound-variable hypothesis builder nfop 3716.
This
shows how the deduction version of a not-free theorem such as nfop 3716
can
be created from the corresponding not-free inference theorem.
(Contributed by NM, 4-Feb-2008.)
|
|
|
Theorem | opid 3718 |
The ordered pair in Kuratowski's representation.
(Contributed by FL, 28-Dec-2011.)
|
|
|
Theorem | ralunsn 3719* |
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 3720* |
Double restricted quantification over the union of a set and a
singleton, using implicit substitution. (Contributed by Paul Chapman,
17-Nov-2012.)
|
|
|
Theorem | opprc 3721 |
Expansion of an ordered pair when either member is a proper class.
(Contributed by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | opprc1 3722 |
Expansion of an ordered pair when the first member is a proper class. See
also opprc 3721. (Contributed by NM, 10-Apr-2004.) (Revised
by Mario
Carneiro, 26-Apr-2015.)
|
|
|
Theorem | opprc2 3723 |
Expansion of an ordered pair when the second member is a proper class.
See also opprc 3721. (Contributed by NM, 15-Nov-1994.) (Revised
by Mario
Carneiro, 26-Apr-2015.)
|
|
|
Theorem | oprcl 3724 |
If an ordered pair has an element, then its arguments are sets.
(Contributed by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | pwsnss 3725 |
The power set of a singleton. (Contributed by Jim Kingdon,
12-Aug-2018.)
|
|
|
Theorem | pwpw0ss 3726 |
Compute the power set of the power set of the empty set. (See pw0 3662
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 3727 |
The power set of an unordered pair. (Contributed by Jim Kingdon,
13-Aug-2018.)
|
|
|
Theorem | pwtpss 3728 |
The power set of an unordered triple. (Contributed by Jim Kingdon,
13-Aug-2018.)
|
|
|
Theorem | pwpwpw0ss 3729 |
Compute the power set of the power set of the power set of the empty set.
(See also pw0 3662 and pwpw0ss 3726.) (Contributed by Jim Kingdon,
13-Aug-2018.)
|
|
|
Theorem | pwv 3730 |
The power class of the universe is the universe. Exercise 4.12(d) of
[Mendelson] p. 235. (Contributed by NM,
14-Sep-2003.)
|
|
|
2.1.18 The union of a class
|
|
Syntax | cuni 3731 |
Extend class notation to include the union of a class (read: 'union
')
|
|
|
Definition | df-uni 3732* |
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 df-un 3070. (Contributed by NM, 23-Aug-1993.)
|
|
|
Theorem | dfuni2 3733* |
Alternate definition of class union. (Contributed by NM,
28-Jun-1998.)
|
|
|
Theorem | eluni 3734* |
Membership in class union. (Contributed by NM, 22-May-1994.)
|
|
|
Theorem | eluni2 3735* |
Membership in class union. Restricted quantifier version. (Contributed
by NM, 31-Aug-1999.)
|
|
|
Theorem | elunii 3736 |
Membership in class union. (Contributed by NM, 24-Mar-1995.)
|
|
|
Theorem | nfuni 3737 |
Bound-variable hypothesis builder for union. (Contributed by NM,
30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | nfunid 3738 |
Deduction version of nfuni 3737. (Contributed by NM, 18-Feb-2013.)
|
|
|
Theorem | csbunig 3739 |
Distribute proper substitution through the union of a class.
(Contributed by Alan Sare, 10-Nov-2012.)
|
|
|
Theorem | unieq 3740 |
Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18.
(Contributed by NM, 10-Aug-1993.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
|
|
Theorem | unieqi 3741 |
Inference of equality of two class unions. (Contributed by NM,
30-Aug-1993.)
|
|
|
Theorem | unieqd 3742 |
Deduction of equality of two class unions. (Contributed by NM,
21-Apr-1995.)
|
|
|
Theorem | eluniab 3743* |
Membership in union of a class abstraction. (Contributed by NM,
11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.)
|
|
|
Theorem | elunirab 3744* |
Membership in union of a class abstraction. (Contributed by NM,
4-Oct-2006.)
|
|
|
Theorem | unipr 3745 |
The union of a pair is the union of its members. Proposition 5.7 of
[TakeutiZaring] p. 16.
(Contributed by NM, 23-Aug-1993.)
|
|
|
Theorem | uniprg 3746 |
The union of a pair is the union of its members. Proposition 5.7 of
[TakeutiZaring] p. 16.
(Contributed by NM, 25-Aug-2006.)
|
|
|
Theorem | unisn 3747 |
A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
(Contributed by NM, 30-Aug-1993.)
|
|
|
Theorem | unisng 3748 |
A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
(Contributed by NM, 13-Aug-2002.)
|
|
|
Theorem | dfnfc2 3749* |
An alternate statement of the effective freeness of a class , when
it is a set. (Contributed by Mario Carneiro, 14-Oct-2016.)
|
|
|
Theorem | uniun 3750 |
The class union of the union of two classes. Theorem 8.3 of [Quine]
p. 53. (Contributed by NM, 20-Aug-1993.)
|
|
|
Theorem | uniin 3751 |
The class union of the intersection of two classes. Exercise 4.12(n) of
[Mendelson] p. 235. (Contributed by
NM, 4-Dec-2003.) (Proof shortened
by Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | uniss 3752 |
Subclass relationship for class union. Theorem 61 of [Suppes] p. 39.
(Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
|
|
Theorem | ssuni 3753 |
Subclass relationship for class union. (Contributed by NM,
24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | unissi 3754 |
Subclass relationship for subclass union. Inference form of uniss 3752.
(Contributed by David Moews, 1-May-2017.)
|
|
|
Theorem | unissd 3755 |
Subclass relationship for subclass union. Deduction form of uniss 3752.
(Contributed by David Moews, 1-May-2017.)
|
|
|
Theorem | uni0b 3756 |
The union of a set is empty iff the set is included in the singleton of
the empty set. (Contributed by NM, 12-Sep-2004.)
|
|
|
Theorem | uni0c 3757* |
The union of a set is empty iff all of its members are empty.
(Contributed by NM, 16-Aug-2006.)
|
|
|
Theorem | uni0 3758 |
The union of the empty set is the empty set. Theorem 8.7 of [Quine]
p. 54. (Reproved without relying on ax-nul by Eric Schmidt.)
(Contributed by NM, 16-Sep-1993.) (Revised by Eric Schmidt,
4-Apr-2007.)
|
|
|
Theorem | elssuni 3759 |
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, 6-Jun-1994.)
|
|
|
Theorem | unissel 3760 |
Condition turning a subclass relationship for union into an equality.
(Contributed by NM, 18-Jul-2006.)
|
|
|
Theorem | unissb 3761* |
Relationship involving membership, subset, and union. Exercise 5 of
[Enderton] p. 26 and its converse.
(Contributed by NM, 20-Sep-2003.)
|
|
|
Theorem | uniss2 3762* |
A subclass condition on the members of two classes that implies a
subclass relation on their unions. Proposition 8.6 of [TakeutiZaring]
p. 59. (Contributed by NM, 22-Mar-2004.)
|
|
|
Theorem | unidif 3763* |
If the difference
contains the largest
members of , then
the union of the difference is the union of . (Contributed by NM,
22-Mar-2004.)
|
|
|
Theorem | ssunieq 3764* |
Relationship implying union. (Contributed by NM, 10-Nov-1999.)
|
|
|
Theorem | unimax 3765* |
Any member of a class is the largest of those members that it includes.
(Contributed by NM, 13-Aug-2002.)
|
|
|
2.1.19 The intersection of a class
|
|
Syntax | cint 3766 |
Extend class notation to include the intersection of a class (read:
'intersect ').
|
|
|
Definition | df-int 3767* |
Define the intersection of a class. Definition 7.35 of [TakeutiZaring]
p. 44. For example, { { 1 , 3 } , { 1 , 8 } } = { 1 } .
Compare this with the intersection of two classes, df-in 3072.
(Contributed by NM, 18-Aug-1993.)
|
|
|
Theorem | dfint2 3768* |
Alternate definition of class intersection. (Contributed by NM,
28-Jun-1998.)
|
|
|
Theorem | inteq 3769 |
Equality law for intersection. (Contributed by NM, 13-Sep-1999.)
|
|
|
Theorem | inteqi 3770 |
Equality inference for class intersection. (Contributed by NM,
2-Sep-2003.)
|
|
|
Theorem | inteqd 3771 |
Equality deduction for class intersection. (Contributed by NM,
2-Sep-2003.)
|
|
|
Theorem | elint 3772* |
Membership in class intersection. (Contributed by NM, 21-May-1994.)
|
|
|
Theorem | elint2 3773* |
Membership in class intersection. (Contributed by NM, 14-Oct-1999.)
|
|
|
Theorem | elintg 3774* |
Membership in class intersection, with the sethood requirement expressed
as an antecedent. (Contributed by NM, 20-Nov-2003.)
|
|
|
Theorem | elinti 3775 |
Membership in class intersection. (Contributed by NM, 14-Oct-1999.)
(Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
|
|
Theorem | nfint 3776 |
Bound-variable hypothesis builder for intersection. (Contributed by NM,
2-Feb-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
|
|
|
Theorem | elintab 3777* |
Membership in the intersection of a class abstraction. (Contributed by
NM, 30-Aug-1993.)
|
|
|
Theorem | elintrab 3778* |
Membership in the intersection of a class abstraction. (Contributed by
NM, 17-Oct-1999.)
|
|
|
Theorem | elintrabg 3779* |
Membership in the intersection of a class abstraction. (Contributed by
NM, 17-Feb-2007.)
|
|
|
Theorem | int0 3780 |
The intersection of the empty set is the universal class. Exercise 2 of
[TakeutiZaring] p. 44.
(Contributed by NM, 18-Aug-1993.)
|
|
|
Theorem | intss1 3781 |
An element of a class includes the intersection of the class. Exercise
4 of [TakeutiZaring] p. 44 (with
correction), generalized to classes.
(Contributed by NM, 18-Nov-1995.)
|
|
|
Theorem | ssint 3782* |
Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52
and its converse. (Contributed by NM, 14-Oct-1999.)
|
|
|
Theorem | ssintab 3783* |
Subclass of the intersection of a class abstraction. (Contributed by
NM, 31-Jul-2006.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
|
|
Theorem | ssintub 3784* |
Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.)
|
|
|
Theorem | ssmin 3785* |
Subclass of the minimum value of class of supersets. (Contributed by
NM, 10-Aug-2006.)
|
|
|
Theorem | intmin 3786* |
Any member of a class is the smallest of those members that include it.
(Contributed by NM, 13-Aug-2002.) (Proof shortened by Andrew Salmon,
9-Jul-2011.)
|
|
|
Theorem | intss 3787 |
Intersection of subclasses. (Contributed by NM, 14-Oct-1999.)
|
|
|
Theorem | intssunim 3788* |
The intersection of an inhabited set is a subclass of its union.
(Contributed by NM, 29-Jul-2006.)
|
|
|
Theorem | ssintrab 3789* |
Subclass of the intersection of a restricted class builder.
(Contributed by NM, 30-Jan-2015.)
|
|
|
Theorem | intssuni2m 3790* |
Subclass relationship for intersection and union. (Contributed by Jim
Kingdon, 14-Aug-2018.)
|
|
|
Theorem | intminss 3791* |
Under subset ordering, the intersection of a restricted class
abstraction is less than or equal to any of its members. (Contributed
by NM, 7-Sep-2013.)
|
|
|
Theorem | intmin2 3792* |
Any set is the smallest of all sets that include it. (Contributed by
NM, 20-Sep-2003.)
|
|
|
Theorem | intmin3 3793* |
Under subset ordering, the intersection of a class abstraction is less
than or equal to any of its members. (Contributed by NM,
3-Jul-2005.)
|
|
|
Theorem | intmin4 3794* |
Elimination of a conjunct in a class intersection. (Contributed by NM,
31-Jul-2006.)
|
|
|
Theorem | intab 3795* |
The intersection of a special case of a class abstraction. may be
free in
and , which can be
thought of a and
. (Contributed by NM, 28-Jul-2006.) (Proof shortened by
Mario Carneiro, 14-Nov-2016.)
|
|
|
Theorem | int0el 3796 |
The intersection of a class containing the empty set is empty.
(Contributed by NM, 24-Apr-2004.)
|
|
|
Theorem | intun 3797 |
The class intersection of the union of two classes. Theorem 78 of
[Suppes] p. 42. (Contributed by NM,
22-Sep-2002.)
|
|
|
Theorem | intpr 3798 |
The intersection of a pair is the intersection of its members. Theorem
71 of [Suppes] p. 42. (Contributed by
NM, 14-Oct-1999.)
|
|
|
Theorem | intprg 3799 |
The intersection of a pair is the intersection of its members. Closed
form of intpr 3798. Theorem 71 of [Suppes] p. 42. (Contributed by FL,
27-Apr-2008.)
|
|
|
Theorem | intsng 3800 |
Intersection of a singleton. (Contributed by Stefan O'Rear,
22-Feb-2015.)
|
|