Theorem List for Intuitionistic Logic Explorer - 3901-4000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | iunxprg 3901* |
A pair index picks out two instances of an indexed union's argument.
(Contributed by Alexander van der Vekens, 2-Feb-2018.)
|
![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif)
![E E](_ce.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![U_ U_](_cupbar.gif) ![{ {](lbrace.gif) ![A A](_ca.gif)
![B B](_cb.gif) ![} }](rbrace.gif)
![( (](lp.gif) ![E E](_ce.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | iunxiun 3902* |
Separate an indexed union in the index of an indexed union.
(Contributed by Mario Carneiro, 5-Dec-2016.)
|
![U_ U_](_cupbar.gif)
![B B](_cb.gif) ![U_ U_](_cupbar.gif) ![U_ U_](_cupbar.gif)
![C C](_cc.gif) |
|
Theorem | iinuniss 3903* |
A relationship involving union and indexed intersection. Exercise 23 of
[Enderton] p. 33 but with equality
changed to subset. (Contributed by
Jim Kingdon, 19-Aug-2018.)
|
![( (](lp.gif) ![|^| |^|](bigcap.gif) ![B B](_cb.gif)
![|^|_ |^|_](_capbar.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) |
|
Theorem | iununir 3904* |
A relationship involving union and indexed union. Exercise 25 of
[Enderton] p. 33 but with biconditional
changed to implication.
(Contributed by Jim Kingdon, 19-Aug-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![U. U.](bigcup.gif) ![B B](_cb.gif) ![U_ U_](_cupbar.gif)
![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sspwuni 3905 |
Subclass relationship for power class and union. (Contributed by NM,
18-Jul-2006.)
|
![( (](lp.gif) ![~P ~P](scrp.gif) ![U. U.](bigcup.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | pwssb 3906* |
Two ways to express a collection of subclasses. (Contributed by NM,
19-Jul-2006.)
|
![( (](lp.gif) ![~P ~P](scrp.gif) ![A. A.](forall.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | elpwpw 3907 |
Characterization of the elements of a double power class: they are exactly
the sets whose union is included in that class. (Contributed by BJ,
29-Apr-2021.)
|
![( (](lp.gif) ![~P ~P](scrp.gif) ![~P ~P](scrp.gif)
![( (](lp.gif) ![U. U.](bigcup.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pwpwab 3908* |
The double power class written as a class abstraction: the class of sets
whose union is included in the given class. (Contributed by BJ,
29-Apr-2021.)
|
![~P
~P](scrp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif)
![U. U.](bigcup.gif) ![A A](_ca.gif) ![} }](rbrace.gif) |
|
Theorem | pwpwssunieq 3909* |
The class of sets whose union is equal to a given class is included in
the double power class of that class. (Contributed by BJ,
29-Apr-2021.)
|
![{
{](lbrace.gif) ![U. U.](bigcup.gif)
![A A](_ca.gif) ![~P
~P](scrp.gif) ![~P ~P](scrp.gif) ![A A](_ca.gif) |
|
Theorem | elpwuni 3910 |
Relationship for power class and union. (Contributed by NM,
18-Jul-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![U. U.](bigcup.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | iinpw 3911* |
The power class of an intersection in terms of indexed intersection.
Exercise 24(a) of [Enderton] p. 33.
(Contributed by NM,
29-Nov-2003.)
|
![~P
~P](scrp.gif) ![|^| |^|](bigcap.gif) ![|^|_ |^|_](_capbar.gif) ![~P ~P](scrp.gif) ![x x](_x.gif) |
|
Theorem | iunpwss 3912* |
Inclusion of an indexed union of a power class in the power class of the
union of its index. Part of Exercise 24(b) of [Enderton] p. 33.
(Contributed by NM, 25-Nov-2003.)
|
![U_ U_](_cupbar.gif)
![~P ~P](scrp.gif)
![~P ~P](scrp.gif) ![U. U.](bigcup.gif) ![A A](_ca.gif) |
|
Theorem | rintm 3913* |
Relative intersection of an inhabited class. (Contributed by Jim
Kingdon, 19-Aug-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![E. E.](exists.gif)
![X X](_cx.gif) ![( (](lp.gif) ![|^| |^|](bigcap.gif) ![X X](_cx.gif) ![|^| |^|](bigcap.gif) ![X X](_cx.gif) ![) )](rp.gif) |
|
2.1.21 Disjointness
|
|
Syntax | wdisj 3914 |
Extend wff notation to include the statement that a family of classes
![B B](_cb.gif) ![( (](lp.gif) ![x
x](_x.gif) , for , is a disjoint family.
|
Disj ![B B](_cb.gif) |
|
Definition | df-disj 3915* |
A collection of classes ![B B](_cb.gif) ![( (](lp.gif) ![x x](_x.gif) is disjoint when for each element
, it is in ![B B](_cb.gif) ![( (](lp.gif) ![x x](_x.gif) for at most
one . (Contributed by
Mario Carneiro, 14-Nov-2016.) (Revised by NM, 16-Jun-2017.)
|
Disj
![A.
A.](forall.gif) ![y y](_y.gif) ![E* E*](_em1.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | dfdisj2 3916* |
Alternate definition for disjoint classes. (Contributed by NM,
17-Jun-2017.)
|
Disj
![A.
A.](forall.gif) ![y y](_y.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | disjss2 3917 |
If each element of a collection is contained in a disjoint collection,
the original collection is also disjoint. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
![( (](lp.gif) ![A. A.](forall.gif) Disj
Disj ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | disjeq2 3918 |
Equality theorem for disjoint collection. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
![( (](lp.gif) ![A. A.](forall.gif) Disj
Disj
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | disjeq2dv 3919* |
Equality deduction for disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![( (](lp.gif) Disj Disj ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | disjss1 3920* |
A subset of a disjoint collection is disjoint. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
![( (](lp.gif) Disj
Disj ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | disjeq1 3921* |
Equality theorem for disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
![( (](lp.gif) Disj
Disj
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | disjeq1d 3922* |
Equality theorem for disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) Disj Disj ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | disjeq12d 3923* |
Equality theorem for disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) Disj
Disj ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | cbvdisj 3924* |
Change bound variables in a disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![( (](lp.gif)
![C C](_cc.gif) Disj
Disj ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | cbvdisjv 3925* |
Change bound variables in a disjoint collection. (Contributed by Mario
Carneiro, 11-Dec-2016.)
|
![( (](lp.gif) ![C C](_cc.gif) Disj Disj ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | nfdisjv 3926* |
Bound-variable hypothesis builder for disjoint collection. (Contributed
by Jim Kingdon, 19-Aug-2018.)
|
![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/ F/](finv.gif) Disj ![B B](_cb.gif) |
|
Theorem | nfdisj1 3927 |
Bound-variable hypothesis builder for disjoint collection. (Contributed
by Mario Carneiro, 14-Nov-2016.)
|
![F/
F/](finv.gif) Disj
![B B](_cb.gif) |
|
Theorem | disjnim 3928* |
If a collection ![B B](_cb.gif) ![( (](lp.gif) ![i i](_i.gif) for is disjoint, then pairs are
disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by
Jim Kingdon, 6-Oct-2022.)
|
![( (](lp.gif) ![C C](_cc.gif) Disj ![A. A.](forall.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | disjnims 3929* |
If a collection ![B B](_cb.gif) ![( (](lp.gif) ![i i](_i.gif) for is disjoint, then pairs are
disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by
Jim Kingdon, 7-Oct-2022.)
|
Disj
![A. A.](forall.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | disji2 3930* |
Property of a disjoint collection: if ![B B](_cb.gif) ![( (](lp.gif) ![X X](_cx.gif) and
![B B](_cb.gif) ![( (](lp.gif) ![Y Y](_cy.gif) , and , then and
are disjoint.
(Contributed by Mario Carneiro, 14-Nov-2016.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif)
![D D](_cd.gif) ![( (](lp.gif) Disj
![( (](lp.gif) ![A A](_ca.gif) ![Y Y](_cy.gif) ![( (](lp.gif) ![D D](_cd.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | invdisj 3931* |
If there is a function ![C C](_cc.gif) ![( (](lp.gif) ![y y](_y.gif) such that ![C C](_cc.gif) ![( (](lp.gif) ![y y](_y.gif) for all
![B B](_cb.gif) ![(
(](lp.gif) ![x x](_x.gif) , then the sets ![B B](_cb.gif) ![( (](lp.gif) ![x x](_x.gif) for distinct
are
disjoint. (Contributed by Mario Carneiro, 10-Dec-2016.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) Disj ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | disjiun 3932* |
A disjoint collection yields disjoint indexed unions for disjoint index
sets. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario
Carneiro, 14-Nov-2016.)
|
![( (](lp.gif) Disj
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![( (](lp.gif) ![U_ U_](_cupbar.gif)
![U_ U_](_cupbar.gif) ![B B](_cb.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | sndisj 3933 |
Any collection of singletons is disjoint. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
Disj ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) |
|
Theorem | 0disj 3934 |
Any collection of empty sets is disjoint. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
Disj ![(/) (/)](varnothing.gif) |
|
Theorem | disjxsn 3935* |
A singleton collection is disjoint. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
Disj ![{ {](lbrace.gif) ![A A](_ca.gif) ![} }](rbrace.gif) ![B B](_cb.gif) |
|
Theorem | disjx0 3936 |
An empty collection is disjoint. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
Disj ![B B](_cb.gif) |
|
2.1.22 Binary relations
|
|
Syntax | wbr 3937 |
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.
|
![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) |
|
Definition | df-br 3938 |
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. This definition of relations 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 (see for
example iprc 4815). (Contributed by NM, 31-Dec-1993.)
|
![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![<. <.](langle.gif) ![A A](_ca.gif)
![B B](_cb.gif) ![R R](_cr.gif) ![) )](rp.gif) |
|
Theorem | breq 3939 |
Equality theorem for binary relations. (Contributed by NM,
4-Jun-1995.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![S S](_cs.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | breq1 3940 |
Equality theorem for a binary relation. (Contributed by NM,
31-Dec-1993.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | breq2 3941 |
Equality theorem for a binary relation. (Contributed by NM,
31-Dec-1993.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | breq12 3942 |
Equality theorem for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | breqi 3943 |
Equality inference for binary relations. (Contributed by NM,
19-Feb-2005.)
|
![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![S S](_cs.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | breq1i 3944 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | breq2i 3945 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | breq12i 3946 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|
![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | breq1d 3947 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | breqd 3948 |
Equality deduction for a binary relation. (Contributed by NM,
29-Oct-2011.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![B B](_cb.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | breq2d 3949 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | breq12d 3950 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | breq123d 3951 |
Equality deduction for a binary relation. (Contributed by NM,
29-Oct-2011.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![S S](_cs.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | breqdi 3952 |
Equality deduction for a binary relation. (Contributed by Thierry
Arnoux, 5-Oct-2020.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![A A](_ca.gif) ![D D](_cd.gif) ![( (](lp.gif) ![C C](_cc.gif) ![B B](_cb.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | breqan12d 3953 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps
ps](_psi.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | breqan12rd 3954 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nbrne1 3955 |
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3-Jun-2012.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | nbrne2 3956 |
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3-Jun-2012.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | eqbrtri 3957 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
![B B](_cb.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) |
|
Theorem | eqbrtrd 3958 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 8-Oct-1999.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | eqbrtrri 3959 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif) |
|
Theorem | eqbrtrrd 3960 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![( (](lp.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | breqtri 3961 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
![A A](_ca.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) |
|
Theorem | breqtrd 3962 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | breqtrri 3963 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
![A A](_ca.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) |
|
Theorem | breqtrrd 3964 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | 3brtr3i 3965 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11-Aug-1999.)
|
![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![D D](_cd.gif) |
|
Theorem | 3brtr4i 3966 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11-Aug-1999.)
|
![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![D D](_cd.gif) |
|
Theorem | 3brtr3d 3967 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 18-Oct-1999.)
|
![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | 3brtr4d 3968 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 21-Feb-2005.)
|
![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | 3brtr3g 3969 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16-Jan-1997.)
|
![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | 3brtr4g 3970 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16-Jan-1997.)
|
![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | eqbrtrid 3971 |
B chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
![( (](lp.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | eqbrtrrid 3972 |
B chained equality inference for a binary relation. (Contributed by NM,
17-Sep-2004.)
|
![( (](lp.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | breqtrid 3973 |
B chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
![A A](_ca.gif) ![R R](_cr.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | breqtrrid 3974 |
B chained equality inference for a binary relation. (Contributed by NM,
24-Apr-2005.)
|
![A A](_ca.gif) ![R R](_cr.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | eqbrtrdi 3975 |
A chained equality inference for a binary relation. (Contributed by NM,
12-Oct-1999.)
|
![( (](lp.gif) ![B B](_cb.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | eqbrtrrdi 3976 |
A chained equality inference for a binary relation. (Contributed by NM,
4-Jan-2006.)
|
![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | breqtrdi 3977 |
A chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | breqtrrdi 3978 |
A chained equality inference for a binary relation. (Contributed by NM,
24-Apr-2005.)
|
![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ssbrd 3979 |
Deduction from a subclass relationship of binary relations.
(Contributed by NM, 30-Apr-2004.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![B B](_cb.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ssbri 3980 |
Inference from a subclass relationship of binary relations.
(Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro,
8-Feb-2015.)
|
![( (](lp.gif) ![C C](_cc.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![B B](_cb.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | nfbrd 3981 |
Deduction version of bound-variable hypothesis builder nfbr 3982.
(Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro,
14-Oct-2016.)
|
![( (](lp.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![A A](_ca.gif) ![( (](lp.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![R R](_cr.gif) ![( (](lp.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![B B](_cb.gif) ![( (](lp.gif)
![F/ F/](finv.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | nfbr 3982 |
Bound-variable hypothesis builder for binary relation. (Contributed by
NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/
F/](finv.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) |
|
Theorem | brab1 3983* |
Relationship between a binary relation and a class abstraction.
(Contributed by Andrew Salmon, 8-Jul-2011.)
|
![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
|
Theorem | br0 3984 |
The empty binary relation never holds. (Contributed by NM,
23-Aug-2018.)
|
![A A](_ca.gif) ![(/) (/)](varnothing.gif) ![B B](_cb.gif) |
|
Theorem | brne0 3985 |
If two sets are in a binary relation, the relation cannot be empty. In
fact, the relation is also inhabited, as seen at brm 3986.
(Contributed by
Alexander van der Vekens, 7-Jul-2018.)
|
![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | brm 3986* |
If two sets are in a binary relation, the relation is inhabited.
(Contributed by Jim Kingdon, 31-Dec-2023.)
|
![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![E. E.](exists.gif) ![R R](_cr.gif) ![) )](rp.gif) |
|
Theorem | brun 3987 |
The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![S S](_cs.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | brin 3988 |
The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![S S](_cs.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | brdif 3989 |
The difference of two binary relations. (Contributed by Scott Fenton,
11-Apr-2011.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![S S](_cs.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sbcbrg 3990 |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![R R](_cr.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sbcbr12g 3991* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sbcbr1g 3992* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sbcbr2g 3993* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | brralrspcev 3994* |
Restricted existential specialization with a restricted universal
quantifier over a relation, closed form. (Contributed by AV,
20-Aug-2022.)
|
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![x x](_x.gif) ![) )](rp.gif) |
|
Theorem | brimralrspcev 3995* |
Restricted existential specialization with a restricted universal
quantifier over an implication with a relation in the antecedent, closed
form. (Contributed by AV, 20-Aug-2022.)
|
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![E. E.](exists.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
2.1.23 Ordered-pair class abstractions (class
builders)
|
|
Syntax | copab 3996 |
Extend class notation to include ordered-pair class abstraction (class
builder).
|
![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![} }](rbrace.gif) |
|
Syntax | cmpt 3997 |
Extend the definition of a class to include maps-to notation for defining
a function via a rule.
|
![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Definition | df-opab 3998* |
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. The brace notation
is called "class abstraction" by Quine; it is also (more
commonly)
called a "class builder" in the literature. (Contributed by
NM,
4-Jul-1994.)
|
![{
{](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif)
![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Definition | df-mpt 3999* |
Define maps-to notation for defining a function via a rule. Read as
"the function defined by the map from (in ) to
![B B](_cb.gif) ![( (](lp.gif) ![x x](_x.gif) ." The class expression is the value of the function
at and normally
contains the variable .
Similar to the
definition of mapping in [ChoquetDD]
p. 2. (Contributed by NM,
17-Feb-2008.)
|
![( (](lp.gif) ![B B](_cb.gif)
![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | opabss 4000* |
The collection of ordered pairs in a class is a subclass of it.
(Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon,
9-Jul-2011.)
|
![{
{](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![x x](_x.gif) ![R R](_cr.gif) ![y y](_y.gif)
![R R](_cr.gif) |