Theorem List for New Foundations Explorer - 4601-4700 *Has distinct variable
group(s)
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,
3-Feb-2015.)
|
Proj2
|
|
Theorem | opth 4602 |
The ordered pair theorem. Two ordered pairs are equal iff their
components are equal. (Contributed by SF, 2-Jan-2015.)
|
|
|
Theorem | opexb 4603 |
An ordered pair is a set iff its components are sets. (Contributed by SF,
2-Jan-2015.)
|
|
|
Theorem | nfop 4604 |
Bound-variable hypothesis builder for ordered pairs. (Contributed by
SF, 2-Jan-2015.)
|
|
|
Theorem | nfopd 4605 |
Deduction version of bound-variable hypothesis builder nfop 4604.
(Contributed by SF, 2-Jan-2015.)
|
|
|
Theorem | eqvinop 4606* |
A variable introduction law for ordered pairs. Analog of Lemma 15 of
[Monk2] p. 109. (Contributed by NM,
28-May-1995.)
|
|
|
Theorem | copsexg 4607* |
Substitution of class for ordered pair .
(Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon,
25-Jul-2011.)
|
|
|
Theorem | copsex2t 4608* |
Closed theorem form of copsex2g 4609. (Contributed by NM,
17-Feb-2013.)
|
|
|
Theorem | copsex2g 4609* |
Implicit substitution inference for ordered pairs. (Contributed by NM,
28-May-1995.)
|
|
|
Theorem | copsex4g 4610* |
An implicit substitution inference for 2 ordered pairs. (Contributed by
NM, 5-Aug-1995.)
|
|
|
Theorem | eqop 4611* |
Express equality to an ordered pair. (Contributed by SF,
6-Jan-2015.)
|
Phi
Phi 0c |
|
Theorem | mosubopt 4612* |
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28-Aug-2007.)
|
|
|
Theorem | mosubop 4613* |
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28-May-1995.)
|
|
|
Theorem | phiun 4614 |
The phi operation distributes over union. (Contributed by SF,
20-Feb-2015.)
|
Phi Phi Phi
|
|
Theorem | phidisjnn 4615 |
The phi operation applied to a set disjoint from the naturals has no
effect. (Contributed by SF, 20-Feb-2015.)
|
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, 14-Apr-2021.)
|
Nn 0c Phi |
|
Theorem | phialllem2 4617* |
Lemma for phiall 4618. Any set without 0c is
equal to the Phi of
a set. (Contributed by Scott Fenton, 8-Apr-2021.)
|
0c Phi |
|
Theorem | phiall 4618* |
Any set is equal to either the Phi of another
set or to a Phi
with 0c adjoined. (Contributed by Scott Fenton,
8-Apr-2021.)
|
Phi
Phi 0c |
|
Theorem | opeq 4619 |
Any class is equal to an ordered pair. (Contributed by Scott Fenton,
8-Apr-2021.)
|
Proj1 Proj2 |
|
Theorem | opeqexb 4620* |
A class is a set iff it is equal to an ordered pair. (Contributed by
Scott Fenton, 19-Apr-2021.)
|
|
|
Theorem | opeqex 4621* |
Any set is equal to some ordered pair. (Contributed by Scott Fenton,
16-Apr-2021.)
|
|
|
2.3.2 Ordered-pair class abstractions (class
builders)
|
|
Syntax | copab 4622 |
Extend class notation to include ordered-pair class abstraction (class
builder).
|
|
|
Definition | df-opab 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, 12-Jan-2015.)
|
|
|
Theorem | opabbid 4624 |
Equivalent wff's yield equal ordered-pair class abstractions (deduction
rule). (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew
Salmon, 9-Jul-2011.)
|
|
|
Theorem | opabbidv 4625* |
Equivalent wff's yield equal ordered-pair class abstractions (deduction
rule). (Contributed by NM, 15-May-1995.)
|
|
|
Theorem | opabbii 4626 |
Equivalent wff's yield equal class abstractions. (Contributed by NM,
15-May-1995.)
|
|
|
Theorem | nfopab 4627* |
Bound-variable hypothesis builder for class abstraction. (Contributed
by NM, 1-Sep-1999.) (Unnecessary distinct variable restrictions were
removed by Andrew Salmon, 11-Jul-2011.)
|
|
|
Theorem | nfopab1 4628 |
The first abstraction variable in an ordered-pair class abstraction
(class builder) is effectively not free. (Contributed by NM,
16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
|
|
Theorem | nfopab2 4629 |
The second abstraction variable in an ordered-pair class abstraction
(class builder) is effectively not free. (Contributed by NM,
16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
|
|
Theorem | cbvopab 4630* |
Rule used to change bound variables in an ordered-pair class
abstraction, using implicit substitution. (Contributed by NM,
14-Sep-2003.)
|
|
|
Theorem | cbvopabv 4631* |
Rule used to change bound variables in an ordered-pair class
abstraction, using implicit substitution. (Contributed by NM,
15-Oct-1996.)
|
|
|
Theorem | cbvopab1 4632* |
Change first bound variable in an ordered-pair class abstraction, using
explicit substitution. (Contributed by NM, 6-Oct-2004.) (Revised by
Mario Carneiro, 14-Oct-2016.)
|
|
|
Theorem | cbvopab2 4633* |
Change second bound variable in an ordered-pair class abstraction, using
explicit substitution. (Contributed by NM, 22-Aug-2013.)
|
|
|
Theorem | cbvopab1s 4634* |
Change first bound variable in an ordered-pair class abstraction, using
explicit substitution. (Contributed by NM, 31-Jul-2003.)
|
|
|
Theorem | cbvopab1v 4635* |
Rule used to change the first bound variable in an ordered pair
abstraction, using implicit substitution. (Contributed by NM,
31-Jul-2003.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|
|
|
Theorem | cbvopab2v 4636* |
Rule used to change the second bound variable in an ordered pair
abstraction, using implicit substitution. (Contributed by NM,
2-Sep-1999.)
|
|
|
Theorem | csbopabg 4637* |
Move substitution into a class abstraction. (Contributed by NM,
6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|
|
|
Theorem | unopab 4638 |
Union of two ordered pair class abstractions. (Contributed by NM,
30-Sep-2002.)
|
|
|
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 | df-br 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
well-defined, 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, 4-Jun-1995.)
|
|
|
Theorem | breq 4641 |
Equality theorem for binary relations. (Contributed by NM,
4-Jun-1995.)
|
|
|
Theorem | breq1 4642 |
Equality theorem for a binary relation. (Contributed by NM,
31-Dec-1993.)
|
|
|
Theorem | breq2 4643 |
Equality theorem for a binary relation. (Contributed by NM,
31-Dec-1993.)
|
|
|
Theorem | breq12 4644 |
Equality theorem for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
|
|
Theorem | breqi 4645 |
Equality inference for binary relations. (Contributed by NM,
19-Feb-2005.)
|
|
|
Theorem | breq1i 4646 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
|
|
Theorem | breq2i 4647 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
|
|
Theorem | breq12i 4648 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.) (Revised by Eric Schmidt, 4-Apr-2007.)
|
|
|
Theorem | breq1d 4649 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
|
|
Theorem | breqd 4650 |
Equality deduction for a binary relation. (Contributed by NM,
29-Oct-2011.)
|
|
|
Theorem | breq2d 4651 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
|
|
Theorem | breq12d 4652 |
Equality deduction for a binary relation. (The proof was shortened by
Andrew Salmon, 9-Jul-2011.) (Contributed by NM, 8-Feb-1996.)
(Revised by set.mm contributors, 9-Jul-2011.)
|
|
|
Theorem | breq123d 4653 |
Equality deduction for a binary relation. (Contributed by NM,
29-Oct-2011.)
|
|
|
Theorem | breqan12d 4654 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
|
|
Theorem | breqan12rd 4655 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
|
|
Theorem | nbrne1 4656 |
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3-Jun-2012.)
|
|
|
Theorem | nbrne2 4657 |
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3-Jun-2012.)
|
|
|
Theorem | eqbrtri 4658 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
|
|
Theorem | eqbrtrd 4659 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 8-Oct-1999.)
|
|
|
Theorem | eqbrtrri 4660 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
|
|
Theorem | eqbrtrrd 4661 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
|
|
Theorem | breqtri 4662 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
|
|
Theorem | breqtrd 4663 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
|
|
Theorem | breqtrri 4664 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
|
|
Theorem | breqtrrd 4665 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
|
|
Theorem | 3brtr3i 4666 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11-Aug-1999.)
|
|
|
Theorem | 3brtr4i 4667 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11-Aug-1999.)
|
|
|
Theorem | 3brtr3d 4668 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 18-Oct-1999.)
|
|
|
Theorem | 3brtr4d 4669 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 21-Feb-2005.)
|
|
|
Theorem | 3brtr3g 4670 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16-Jan-1997.)
|
|
|
Theorem | 3brtr4g 4671 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16-Jan-1997.)
|
|
|
Theorem | syl5eqbr 4672 |
B chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
|
|
Theorem | syl5eqbrr 4673 |
B chained equality inference for a binary relation. (Contributed by NM,
17-Sep-2004.)
|
|
|
Theorem | syl5breq 4674 |
B chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
|
|
Theorem | syl5breqr 4675 |
B chained equality inference for a binary relation. (Contributed by NM,
24-Apr-2005.)
|
|
|
Theorem | syl6eqbr 4676 |
A chained equality inference for a binary relation. (Contributed by NM,
12-Oct-1999.)
|
|
|
Theorem | syl6eqbrr 4677 |
A chained equality inference for a binary relation. (Contributed by NM,
4-Jan-2006.)
|
|
|
Theorem | syl6breq 4678 |
A chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
|
|
Theorem | syl6breqr 4679 |
A chained equality inference for a binary relation. (Contributed by NM,
24-Apr-2005.)
|
|
|
Theorem | ssbrd 4680 |
Deduction from a subclass relationship of binary relations.
(Contributed by NM, 30-Apr-2004.)
|
|
|
Theorem | ssbri 4681 |
Inference from a subclass relationship of binary relations. (The proof
was shortened by Andrew Salmon, 9-Jul-2011.) (Contributed by NM,
28-Mar-2007.) (Revised by set.mm contributors, 9-Jul-2011.)
|
|
|
Theorem | nfbrd 4682 |
Deduction version of bound-variable hypothesis builder nfbr 4683.
(Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro,
14-Oct-2016.)
|
|
|
Theorem | nfbr 4683 |
Bound-variable hypothesis builder for binary relation. (Contributed by
NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
|
|
Theorem | brab1 4684* |
Relationship between a binary relation and a class abstraction.
(Contributed by Andrew Salmon, 8-Jul-2011.)
|
|
|
Theorem | sbcbrg 4685 |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
|
|
Theorem | sbcbr12g 4686* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
|
|
Theorem | sbcbr1g 4687* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
|
|
Theorem | sbcbr2g 4688* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
|
|
Theorem | brex 4689 |
Binary relationship implies sethood of both parts. (Contributed by SF,
7-Jan-2015.)
|
|
|
Theorem | brreldmex 4690 |
Binary relationship implies sethood of domain. (Contributed by SF,
7-Jan-2018.)
|
|
|
Theorem | brrelrnex 4691 |
Binary relationship implies sethood of range. (Contributed by SF,
7-Jan-2018.)
|
|
|
Theorem | brun 4692 |
The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
|
|
|
Theorem | brin 4693 |
The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
|
|
|
Theorem | brdif 4694 |
The difference of two binary relations. (Contributed by Scott Fenton,
11-Apr-2011.)
|
|
|
2.3.4 Ordered-pair 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, 25-Jul-2011.) (Contributed
by NM, 14-Apr-1995.) (Revised by set.mm contributors, 25-Jul-2011.)
|
|
|
Theorem | elopab 4696* |
Membership in a class abstraction of pairs. (Contributed by NM,
24-Mar-1998.)
|
|
|
Theorem | opelopabsb 4697* |
The law of concretion in terms of substitutions. (Contributed by NM,
30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
|
|
|
Theorem | brabsb 4698* |
The law of concretion in terms of substitutions. (Contributed by NM,
17-Mar-2008.)
|
|
|
Theorem | opelopabt 4699* |
Closed theorem form of opelopab 4708. (Contributed by NM,
19-Feb-2013.)
|
|
|
Theorem | opelopabga 4700* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
Mario Carneiro, 19-Dec-2013.)
|
|