Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  pwpwpw0ss 3541 
Compute the power set of the power set of the power set of the empty
set. (See also pw0 3474 and pwpw0ss 3538.) (Contributed by Jim Kingdon,
13Aug2018.)



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



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



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



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



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



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



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



Theorem  nfunid 3550 
Deduction version of nfuni 3549. (Contributed by NM, 18Feb2013.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  uniss2 3574* 
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 3575* 
If the difference
contains the largest
members of , then
the union of the difference is the union of . (Contributed by NM,
22Mar2004.)



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



Theorem  unimax 3577* 
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 3578 
Extend class notation to include the intersection of a class (read:
'intersect ').



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  intss1 3593 
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 3594* 
Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52
and its converse. (Contributed by NM, 14Oct1999.)



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



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



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



Theorem  intmin 3598* 
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 3599 
Intersection of subclasses. (Contributed by NM, 14Oct1999.)



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

