Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  pwpwpw0ss 3634 
Compute the power set of the power set of the power set of the empty set.
(See also pw0 3567 and pwpw0ss 3631.) (Contributed by Jim Kingdon,
13Aug2018.)



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



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



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



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



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



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



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



Theorem  nfunid 3643 
Deduction version of nfuni 3642. (Contributed by NM, 18Feb2013.)



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  uniin 3656 
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 3657 
Subclass relationship for class union. Theorem 61 of [Suppes] p. 39.
(Contributed by NM, 22Mar1998.) (Proof shortened by Andrew Salmon,
29Jun2011.)



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



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



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



Theorem  uni0b 3661 
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 3662* 
The union of a set is empty iff all of its members are empty.
(Contributed by NM, 16Aug2006.)



Theorem  uni0 3663 
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 3664 
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 3665 
Condition turning a subclass relationship for union into an equality.
(Contributed by NM, 18Jul2006.)



Theorem  unissb 3666* 
Relationship involving membership, subset, and union. Exercise 5 of
[Enderton] p. 26 and its converse.
(Contributed by NM, 20Sep2003.)



Theorem  uniss2 3667* 
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, 22Mar2004.)



Theorem  unidif 3668* 
If the difference
contains the largest
members of , then
the union of the difference is the union of . (Contributed by NM,
22Mar2004.)



Theorem  ssunieq 3669* 
Relationship implying union. (Contributed by NM, 10Nov1999.)



Theorem  unimax 3670* 
Any member of a class is the largest of those members that it includes.
(Contributed by NM, 13Aug2002.)



2.1.19 The intersection of a class


Syntax  cint 3671 
Extend class notation to include the intersection of a class (read:
'intersect ').



Definition  dfint 3672* 
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, dfin 2994.
(Contributed by NM, 18Aug1993.)



Theorem  dfint2 3673* 
Alternate definition of class intersection. (Contributed by NM,
28Jun1998.)



Theorem  inteq 3674 
Equality law for intersection. (Contributed by NM, 13Sep1999.)



Theorem  inteqi 3675 
Equality inference for class intersection. (Contributed by NM,
2Sep2003.)



Theorem  inteqd 3676 
Equality deduction for class intersection. (Contributed by NM,
2Sep2003.)



Theorem  elint 3677* 
Membership in class intersection. (Contributed by NM, 21May1994.)



Theorem  elint2 3678* 
Membership in class intersection. (Contributed by NM, 14Oct1999.)



Theorem  elintg 3679* 
Membership in class intersection, with the sethood requirement expressed
as an antecedent. (Contributed by NM, 20Nov2003.)



Theorem  elinti 3680 
Membership in class intersection. (Contributed by NM, 14Oct1999.)
(Proof shortened by Andrew Salmon, 9Jul2011.)



Theorem  nfint 3681 
Boundvariable hypothesis builder for intersection. (Contributed by NM,
2Feb1997.) (Proof shortened by Andrew Salmon, 12Aug2011.)



Theorem  elintab 3682* 
Membership in the intersection of a class abstraction. (Contributed by
NM, 30Aug1993.)



Theorem  elintrab 3683* 
Membership in the intersection of a class abstraction. (Contributed by
NM, 17Oct1999.)



Theorem  elintrabg 3684* 
Membership in the intersection of a class abstraction. (Contributed by
NM, 17Feb2007.)



Theorem  int0 3685 
The intersection of the empty set is the universal class. Exercise 2 of
[TakeutiZaring] p. 44.
(Contributed by NM, 18Aug1993.)



Theorem  intss1 3686 
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, 18Nov1995.)



Theorem  ssint 3687* 
Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52
and its converse. (Contributed by NM, 14Oct1999.)



Theorem  ssintab 3688* 
Subclass of the intersection of a class abstraction. (Contributed by
NM, 31Jul2006.) (Proof shortened by Andrew Salmon, 9Jul2011.)



Theorem  ssintub 3689* 
Subclass of the least upper bound. (Contributed by NM, 8Aug2000.)



Theorem  ssmin 3690* 
Subclass of the minimum value of class of supersets. (Contributed by
NM, 10Aug2006.)



Theorem  intmin 3691* 
Any member of a class is the smallest of those members that include it.
(Contributed by NM, 13Aug2002.) (Proof shortened by Andrew Salmon,
9Jul2011.)



Theorem  intss 3692 
Intersection of subclasses. (Contributed by NM, 14Oct1999.)



Theorem  intssunim 3693* 
The intersection of an inhabited set is a subclass of its union.
(Contributed by NM, 29Jul2006.)



Theorem  ssintrab 3694* 
Subclass of the intersection of a restricted class builder.
(Contributed by NM, 30Jan2015.)



Theorem  intssuni2m 3695* 
Subclass relationship for intersection and union. (Contributed by Jim
Kingdon, 14Aug2018.)



Theorem  intminss 3696* 
Under subset ordering, the intersection of a restricted class
abstraction is less than or equal to any of its members. (Contributed
by NM, 7Sep2013.)



Theorem  intmin2 3697* 
Any set is the smallest of all sets that include it. (Contributed by
NM, 20Sep2003.)



Theorem  intmin3 3698* 
Under subset ordering, the intersection of a class abstraction is less
than or equal to any of its members. (Contributed by NM,
3Jul2005.)



Theorem  intmin4 3699* 
Elimination of a conjunct in a class intersection. (Contributed by NM,
31Jul2006.)



Theorem  intab 3700* 
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, 28Jul2006.) (Proof shortened by
Mario Carneiro, 14Nov2016.)

