Type  Label  Description 
Statement 

Theorem  proj2op 4601 
The second projection operator applied to an ordered pair yields its
second member. Theorem X.2.8 of [Rosser]
p. 283. (Contributed by SF,
3Feb2015.)

Proj2


Theorem  opth 4602 
The ordered pair theorem. Two ordered pairs are equal iff their
components are equal. (Contributed by SF, 2Jan2015.)



Theorem  opexb 4603 
An ordered pair is a set iff its components are sets. (Contributed by SF,
2Jan2015.)



Theorem  nfop 4604 
Boundvariable hypothesis builder for ordered pairs. (Contributed by
SF, 2Jan2015.)



Theorem  nfopd 4605 
Deduction version of boundvariable hypothesis builder nfop 4604.
(Contributed by SF, 2Jan2015.)



Theorem  eqvinop 4606* 
A variable introduction law for ordered pairs. Analog of Lemma 15 of
[Monk2] p. 109. (Contributed by NM,
28May1995.)



Theorem  copsexg 4607* 
Substitution of class for ordered pair .
(Contributed by NM, 27Dec1996.) (Revised by Andrew Salmon,
25Jul2011.)



Theorem  copsex2t 4608* 
Closed theorem form of copsex2g 4609. (Contributed by NM,
17Feb2013.)



Theorem  copsex2g 4609* 
Implicit substitution inference for ordered pairs. (Contributed by NM,
28May1995.)



Theorem  copsex4g 4610* 
An implicit substitution inference for 2 ordered pairs. (Contributed by
NM, 5Aug1995.)



Theorem  eqop 4611* 
Express equality to an ordered pair. (Contributed by SF,
6Jan2015.)

Phi
Phi 0_{c} 

Theorem  mosubopt 4612* 
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28Aug2007.)



Theorem  mosubop 4613* 
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28May1995.)



Theorem  phiun 4614 
The phi operation distributes over union. (Contributed by SF,
20Feb2015.)

Phi Phi Phi


Theorem  phidisjnn 4615 
The phi operation applied to a set disjoint from the naturals has no
effect. (Contributed by SF, 20Feb2015.)

Nn Phi 

Theorem  phialllem1 4616* 
Lemma for phiall 4618. Any set of numbers without zero is the Phi
of a
set. (Contributed by Scott Fenton, 14Apr2021.)

Nn 0_{c} Phi 

Theorem  phialllem2 4617* 
Lemma for phiall 4618. Any set without 0_{c} is
equal to the Phi of
a set. (Contributed by Scott Fenton, 8Apr2021.)

0_{c} Phi 

Theorem  phiall 4618* 
Any set is equal to either the Phi of another
set or to a Phi
with 0_{c} adjoined. (Contributed by Scott Fenton,
8Apr2021.)

Phi
Phi 0_{c} 

Theorem  opeq 4619 
Any class is equal to an ordered pair. (Contributed by Scott Fenton,
8Apr2021.)

Proj1 Proj2 

Theorem  opeqexb 4620* 
A class is a set iff it is equal to an ordered pair. (Contributed by
Scott Fenton, 19Apr2021.)



Theorem  opeqex 4621* 
Any set is equal to some ordered pair. (Contributed by Scott Fenton,
16Apr2021.)



2.3.2 Orderedpair class abstractions (class
builders)


Syntax  copab 4622 
Extend class notation to include orderedpair class abstraction (class
builder).



Definition  dfopab 4623* 
Define the class abstraction of a collection of ordered pairs.
Definition 3.3 of [Monk1] p. 34. Usually
and are distinct,
although the definition doesn't strictly require it (see dfid2 4769 for a
case where they are not distinct). The brace notation is called
"class
abstraction" by Quine; it is also (more commonly) called a
"class
builder" in the literature. (Contributed by SF, 12Jan2015.)



Theorem  opabbid 4624 
Equivalent wff's yield equal orderedpair class abstractions (deduction
rule). (Contributed by NM, 21Feb2004.) (Proof shortened by Andrew
Salmon, 9Jul2011.)



Theorem  opabbidv 4625* 
Equivalent wff's yield equal orderedpair class abstractions (deduction
rule). (Contributed by NM, 15May1995.)



Theorem  opabbii 4626 
Equivalent wff's yield equal class abstractions. (Contributed by NM,
15May1995.)



Theorem  nfopab 4627* 
Boundvariable hypothesis builder for class abstraction. (Contributed
by NM, 1Sep1999.) (Unnecessary distinct variable restrictions were
removed by Andrew Salmon, 11Jul2011.)



Theorem  nfopab1 4628 
The first abstraction variable in an orderedpair class abstraction
(class builder) is effectively not free. (Contributed by NM,
16May1995.) (Revised by Mario Carneiro, 14Oct2016.)



Theorem  nfopab2 4629 
The second abstraction variable in an orderedpair class abstraction
(class builder) is effectively not free. (Contributed by NM,
16May1995.) (Revised by Mario Carneiro, 14Oct2016.)



Theorem  cbvopab 4630* 
Rule used to change bound variables in an orderedpair class
abstraction, using implicit substitution. (Contributed by NM,
14Sep2003.)



Theorem  cbvopabv 4631* 
Rule used to change bound variables in an orderedpair class
abstraction, using implicit substitution. (Contributed by NM,
15Oct1996.)



Theorem  cbvopab1 4632* 
Change first bound variable in an orderedpair class abstraction, using
explicit substitution. (Contributed by NM, 6Oct2004.) (Revised by
Mario Carneiro, 14Oct2016.)



Theorem  cbvopab2 4633* 
Change second bound variable in an orderedpair class abstraction, using
explicit substitution. (Contributed by NM, 22Aug2013.)



Theorem  cbvopab1s 4634* 
Change first bound variable in an orderedpair class abstraction, using
explicit substitution. (Contributed by NM, 31Jul2003.)



Theorem  cbvopab1v 4635* 
Rule used to change the first bound variable in an ordered pair
abstraction, using implicit substitution. (Contributed by NM,
31Jul2003.) (Proof shortened by Eric Schmidt, 4Apr2007.)



Theorem  cbvopab2v 4636* 
Rule used to change the second bound variable in an ordered pair
abstraction, using implicit substitution. (Contributed by NM,
2Sep1999.)



Theorem  csbopabg 4637* 
Move substitution into a class abstraction. (Contributed by NM,
6Aug2007.) (Proof shortened by Mario Carneiro, 17Nov2016.)



Theorem  unopab 4638 
Union of two ordered pair class abstractions. (Contributed by NM,
30Sep2002.)



2.3.3 Binary relations


Syntax  wbr 4639 
Extend wff notation to include the general binary relation predicate.
Note that the syntax is simply three class symbols in a row. Since binary
relations are the only possible wff expressions consisting of three class
expressions in a row, the syntax is unambiguous.



Definition  dfbr 4640 
Define a general binary relation. Note that the syntax is simply three
class symbols in a row. Definition 6.18 of [TakeutiZaring] p. 29
generalized to arbitrary classes. Class normally denotes a relation
that compares two classes and .
This definition is
welldefined, although not very meaningful, when classes and/or
are proper
classes (i.e. are not sets). On the other hand, we often
find uses for this definition when is a proper class. (Contributed
by NM, 4Jun1995.)



Theorem  breq 4641 
Equality theorem for binary relations. (Contributed by NM,
4Jun1995.)



Theorem  breq1 4642 
Equality theorem for a binary relation. (Contributed by NM,
31Dec1993.)



Theorem  breq2 4643 
Equality theorem for a binary relation. (Contributed by NM,
31Dec1993.)



Theorem  breq12 4644 
Equality theorem for a binary relation. (Contributed by NM,
8Feb1996.)



Theorem  breqi 4645 
Equality inference for binary relations. (Contributed by NM,
19Feb2005.)



Theorem  breq1i 4646 
Equality inference for a binary relation. (Contributed by NM,
8Feb1996.)



Theorem  breq2i 4647 
Equality inference for a binary relation. (Contributed by NM,
8Feb1996.)



Theorem  breq12i 4648 
Equality inference for a binary relation. (Contributed by NM,
8Feb1996.) (Revised by Eric Schmidt, 4Apr2007.)



Theorem  breq1d 4649 
Equality deduction for a binary relation. (Contributed by NM,
8Feb1996.)



Theorem  breqd 4650 
Equality deduction for a binary relation. (Contributed by NM,
29Oct2011.)



Theorem  breq2d 4651 
Equality deduction for a binary relation. (Contributed by NM,
8Feb1996.)



Theorem  breq12d 4652 
Equality deduction for a binary relation. (The proof was shortened by
Andrew Salmon, 9Jul2011.) (Contributed by NM, 8Feb1996.)
(Revised by set.mm contributors, 9Jul2011.)



Theorem  breq123d 4653 
Equality deduction for a binary relation. (Contributed by NM,
29Oct2011.)



Theorem  breqan12d 4654 
Equality deduction for a binary relation. (Contributed by NM,
8Feb1996.)



Theorem  breqan12rd 4655 
Equality deduction for a binary relation. (Contributed by NM,
8Feb1996.)



Theorem  nbrne1 4656 
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3Jun2012.)



Theorem  nbrne2 4657 
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3Jun2012.)



Theorem  eqbrtri 4658 
Substitution of equal classes into a binary relation. (Contributed by
NM, 5Aug1993.)



Theorem  eqbrtrd 4659 
Substitution of equal classes into a binary relation. (Contributed by
NM, 8Oct1999.)



Theorem  eqbrtrri 4660 
Substitution of equal classes into a binary relation. (Contributed by
NM, 5Aug1993.)



Theorem  eqbrtrrd 4661 
Substitution of equal classes into a binary relation. (Contributed by
NM, 24Oct1999.)



Theorem  breqtri 4662 
Substitution of equal classes into a binary relation. (Contributed by
NM, 5Aug1993.)



Theorem  breqtrd 4663 
Substitution of equal classes into a binary relation. (Contributed by
NM, 24Oct1999.)



Theorem  breqtrri 4664 
Substitution of equal classes into a binary relation. (Contributed by
NM, 5Aug1993.)



Theorem  breqtrrd 4665 
Substitution of equal classes into a binary relation. (Contributed by
NM, 24Oct1999.)



Theorem  3brtr3i 4666 
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11Aug1999.)



Theorem  3brtr4i 4667 
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11Aug1999.)



Theorem  3brtr3d 4668 
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 18Oct1999.)



Theorem  3brtr4d 4669 
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 21Feb2005.)



Theorem  3brtr3g 4670 
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16Jan1997.)



Theorem  3brtr4g 4671 
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16Jan1997.)



Theorem  syl5eqbr 4672 
B chained equality inference for a binary relation. (Contributed by NM,
11Oct1999.)



Theorem  syl5eqbrr 4673 
B chained equality inference for a binary relation. (Contributed by NM,
17Sep2004.)



Theorem  syl5breq 4674 
B chained equality inference for a binary relation. (Contributed by NM,
11Oct1999.)



Theorem  syl5breqr 4675 
B chained equality inference for a binary relation. (Contributed by NM,
24Apr2005.)



Theorem  syl6eqbr 4676 
A chained equality inference for a binary relation. (Contributed by NM,
12Oct1999.)



Theorem  syl6eqbrr 4677 
A chained equality inference for a binary relation. (Contributed by NM,
4Jan2006.)



Theorem  syl6breq 4678 
A chained equality inference for a binary relation. (Contributed by NM,
11Oct1999.)



Theorem  syl6breqr 4679 
A chained equality inference for a binary relation. (Contributed by NM,
24Apr2005.)



Theorem  ssbrd 4680 
Deduction from a subclass relationship of binary relations.
(Contributed by NM, 30Apr2004.)



Theorem  ssbri 4681 
Inference from a subclass relationship of binary relations. (The proof
was shortened by Andrew Salmon, 9Jul2011.) (Contributed by NM,
28Mar2007.) (Revised by set.mm contributors, 9Jul2011.)



Theorem  nfbrd 4682 
Deduction version of boundvariable hypothesis builder nfbr 4683.
(Contributed by NM, 13Dec2005.) (Revised by Mario Carneiro,
14Oct2016.)



Theorem  nfbr 4683 
Boundvariable hypothesis builder for binary relation. (Contributed by
NM, 1Sep1999.) (Revised by Mario Carneiro, 14Oct2016.)



Theorem  brab1 4684* 
Relationship between a binary relation and a class abstraction.
(Contributed by Andrew Salmon, 8Jul2011.)



Theorem  sbcbrg 4685 
Move substitution in and out of a binary relation. (Contributed by NM,
13Dec2005.) (Proof shortened by Andrew Salmon, 9Jul2011.)



Theorem  sbcbr12g 4686* 
Move substitution in and out of a binary relation. (Contributed by NM,
13Dec2005.)



Theorem  sbcbr1g 4687* 
Move substitution in and out of a binary relation. (Contributed by NM,
13Dec2005.)



Theorem  sbcbr2g 4688* 
Move substitution in and out of a binary relation. (Contributed by NM,
13Dec2005.)



Theorem  brex 4689 
Binary relationship implies sethood of both parts. (Contributed by SF,
7Jan2015.)



Theorem  brreldmex 4690 
Binary relationship implies sethood of domain. (Contributed by SF,
7Jan2018.)



Theorem  brrelrnex 4691 
Binary relationship implies sethood of range. (Contributed by SF,
7Jan2018.)



Theorem  brun 4692 
The union of two binary relations. (Contributed by NM, 21Dec2008.)



Theorem  brin 4693 
The intersection of two relations. (Contributed by FL, 7Oct2008.)



Theorem  brdif 4694 
The difference of two binary relations. (Contributed by Scott Fenton,
11Apr2011.)



2.3.4 Orderedpair class abstractions
(cont.)


Theorem  opabid 4695 
The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61.
(The proof was shortened by Andrew Salmon, 25Jul2011.) (Contributed
by NM, 14Apr1995.) (Revised by set.mm contributors, 25Jul2011.)



Theorem  elopab 4696* 
Membership in a class abstraction of pairs. (Contributed by NM,
24Mar1998.)



Theorem  opelopabsb 4697* 
The law of concretion in terms of substitutions. (Contributed by NM,
30Sep2002.) (Revised by Mario Carneiro, 18Nov2016.)



Theorem  brabsb 4698* 
The law of concretion in terms of substitutions. (Contributed by NM,
17Mar2008.)



Theorem  opelopabt 4699* 
Closed theorem form of opelopab 4708. (Contributed by NM,
19Feb2013.)



Theorem  opelopabga 4700* 
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
Mario Carneiro, 19Dec2013.)

