P. 47 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4601-4700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iinxprg 4601*	Indexed intersection with an unordered pair index. (Contributed by NM, 25-Jan-2012.)
|- ( x = A -> C = D )   &    |- ( x = B -> C = E )   =>    |- ( ( A e. V /\ B e. W ) -> |^|_ x e. { A , B } C = ( D i^i E ) )
Theorem	iunxsng 4602*	A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.)
|- ( x = A -> B = C )   =>    |- ( A e. V -> U_ x e. { A } B = C )
Theorem	iunxsn 4603*	A singleton index picks out an instance of an indexed union's argument. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 25-Jun-2016.)
|- A e. _V   &    |- ( x = A -> B = C )   =>    |- U_ x e. { A } B = C
Theorem	iunun 4604	Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|- U_ x e. A ( B u. C ) = ( U_ x e. A B u. U_ x e. A C )
Theorem	iunxun 4605	Separate a union in the index of an indexed union. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|- U_ x e. ( A u. B ) C = ( U_ x e. A C u. U_ x e. B C )
Theorem	iunxdif3 4606*	An indexed union where some terms are the empty set. See iunxdif2 4568. (Contributed by Thierry Arnoux, 4-May-2020.)
|- F/_ x E   =>    |- ( A. x e. E B = (/) -> U_ x e. ( A \ E ) B = U_ x e. A B )
Theorem	iunxprg 4607*	A pair index picks out two instances of an indexed union's argument. (Contributed by Alexander van der Vekens, 2-Feb-2018.)
|- ( x = A -> C = D )   &    |- ( x = B -> C = E )   =>    |- ( ( A e. V /\ B e. W ) -> U_ x e. { A , B } C = ( D u. E ) )
Theorem	iunxiun 4608*	Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016.)
|- U_ x e. U_ y e. A B C = U_ y e. A U_ x e. B C
Theorem	iinuni 4609*	A relationship involving union and indexed intersection. Exercise 23 of [Enderton] p. 33. (Contributed by NM, 25-Nov-2003.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|- ( A u. |^| B ) = |^|_ x e. B ( A u. x )
Theorem	iununi 4610*	A relationship involving union and indexed union. Exercise 25 of [Enderton] p. 33. (Contributed by NM, 25-Nov-2003.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|- ( ( B = (/) -> A = (/) ) <-> ( A u. U. B ) = U_ x e. B ( A u. x ) )
Theorem	sspwuni 4611	Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
|- ( A C_ ~P B <-> U. A C_ B )
Theorem	pwssb 4612*	Two ways to express a collection of subclasses. (Contributed by NM, 19-Jul-2006.)
|- ( A C_ ~P B <-> A. x e. A x C_ B )
Theorem	elpwpw 4613	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.)
|- ( A e. ~P ~P B <-> ( A e. _V /\ U. A C_ B ) )
Theorem	pwpwab 4614*	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 A = { x | U. x C_ A }
Theorem	pwpwssunieq 4615*	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.)
|- { x | U. x = A } C_ ~P ~P A
Theorem	elpwuni 4616	Relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
|- ( B e. A -> ( A C_ ~P B <-> U. A = B ) )
Theorem	iinpw 4617*	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 |^| A = |^|_ x e. A ~P x
Theorem	iunpwss 4618*	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_ x e. A ~P x C_ ~P U. A
Theorem	rintn0 4619	Relative intersection of a nonempty set. (Contributed by Stefan O'Rear, 3-Apr-2015.) (Revised by Mario Carneiro, 5-Jun-2015.)
|- ( ( X C_ ~P A /\ X =/= (/) ) -> ( A i^i |^| X ) = |^| X )
2.1.21  Disjointness
Syntax	wdisj 4620	Extend wff notation to include the statement that a family of classes B ( x ), for x e. A, is a disjoint family.
wff Disj x e. A B
Definition	df-disj 4621*	A collection of classes B ( x ) is disjoint when for each element y, it is in B ( x ) for at most one x. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by NM, 16-Jun-2017.)
|- (Disj x e. A B <-> A. y E* x e. A y e. B )
Theorem	dfdisj2 4622*	Alternate definition for disjoint classes. (Contributed by NM, 17-Jun-2017.)
|- (Disj x e. A B <-> A. y E* x ( x e. A /\ y e. B ) )
Theorem	disjss2 4623	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.)
|- ( A. x e. A B C_ C -> (Disj x e. A C -> Disj x e. A B ) )
Theorem	disjeq2 4624	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( A. x e. A B = C -> (Disj x e. A B <-> Disj x e. A C ) )
Theorem	disjeq2dv 4625*	Equality deduction for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> (Disj x e. A B <-> Disj x e. A C ) )
Theorem	disjss1 4626*	A subset of a disjoint collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( A C_ B -> (Disj x e. B C -> Disj x e. A C ) )
Theorem	disjeq1 4627*	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( A = B -> (Disj x e. A C <-> Disj x e. B C ) )
Theorem	disjeq1d 4628*	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( ph -> A = B )   =>    |- ( ph -> (Disj x e. A C <-> Disj x e. B C ) )
Theorem	disjeq12d 4629*	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> (Disj x e. A C <-> Disj x e. B D ) )
Theorem	cbvdisj 4630*	Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- F/_ y B   &    |- F/_ x C   &    |- ( x = y -> B = C )   =>    |- (Disj x e. A B <-> Disj y e. A C )
Theorem	cbvdisjv 4631*	Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 11-Dec-2016.)
|- ( x = y -> B = C )   =>    |- (Disj x e. A B <-> Disj y e. A C )
Theorem	nfdisj 4632	Bound-variable hypothesis builder for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- F/_ y A   &    |- F/_ y B   =>    |- F/ yDisj x e. A B
Theorem	nfdisj1 4633	Bound-variable hypothesis builder for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- F/ xDisj x e. A B
Theorem	disjor 4634*	Two ways to say that a collection B ( i ) for i e. A is disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 14-Nov-2016.)
|- ( i = j -> B = C )   =>    |- (Disj i e. A B <-> A. i e. A A. j e. A ( i = j \/ ( B i^i C ) = (/) ) )
Theorem	disjors 4635*	Two ways to say that a collection B ( i ) for i e. A is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- (Disj x e. A B <-> A. i e. A A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
Theorem	disji2 4636*	Property of a disjoint collection: if B ( X ) = C and B ( Y ) = D, and X =/= Y, then C and D are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( x = X -> B = C )   &    |- ( x = Y -> B = D )   =>    |- ( (Disj x e. A B /\ ( X e. A /\ Y e. A ) /\ X =/= Y ) -> ( C i^i D ) = (/) )
Theorem	disji 4637*	Property of a disjoint collection: if B ( X ) = C and B ( Y ) = D have a common element Z, then X = Y. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( x = X -> B = C )   &    |- ( x = Y -> B = D )   =>    |- ( (Disj x e. A B /\ ( X e. A /\ Y e. A ) /\ ( Z e. C /\ Z e. D ) ) -> X = Y )
Theorem	invdisj 4638*	If there is a function C ( y ) such that C ( y ) = x for all y e. B ( x ), then the sets B ( x ) for distinct x e. A are disjoint. (Contributed by Mario Carneiro, 10-Dec-2016.)
|- ( A. x e. A A. y e. B C = x -> Disj x e. A B )
Theorem	invdisjrab 4639*	The restricted class abstractions { x e. B | C = y } for distinct y e. A are disjoint. (Contributed by AV, 6-May-2020.)
|- Disj y e. A { x e. B | C = y }
Theorem	disjiun 4640*	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.)
|- ( (Disj x e. A B /\ ( C C_ A /\ D C_ A /\ ( C i^i D ) = (/) ) ) -> ( U_ x e. C B i^i U_ x e. D B ) = (/) )
Theorem	disjord 4641*	Conditions for a collection of sets A ( a ) for a e. V to be disjoint. (Contributed by AV, 9-Jan-2022.)
|- ( a = b -> A = B )   &    |- ( ( ph /\ x e. A /\ x e. B ) -> a = b )   =>    |- ( ph -> Disj a e. V A )
Theorem	disjiunb 4642*	Two ways to say that a collection of index unions C ( i , x ) for i e. A and x e. B is disjoint. (Contributed by AV, 9-Jan-2022.)
|- ( i = j -> B = D )   &    |- ( i = j -> C = E )   =>    |- (Disj i e. A U_ x e. B C <-> A. i e. A A. j e. A ( i = j \/ ( U_ x e. B C i^i U_ x e. D E ) = (/) ) )
Theorem	disjiund 4643*	Conditions for a collection of index unions of sets A ( a , b ) for a e. V and b e. W to be disjoint. (Contributed by AV, 9-Jan-2022.)
|- ( a = c -> A = C )   &    |- ( b = d -> C = D )   &    |- ( a = c -> W = X )   &    |- ( ( ph /\ x e. A /\ x e. D ) -> a = c )   =>    |- ( ph -> Disj a e. V U_ b e. W A )
Theorem	sndisj 4644	Any collection of singletons is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- Disj x e. A { x }
Theorem	0disj 4645	Any collection of empty sets is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- Disj x e. A (/)
Theorem	disjxsn 4646*	A singleton collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- Disj x e. { A } B
Theorem	disjx0 4647	An empty collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- Disj x e. (/) B
Theorem	disjprg 4648*	A pair collection is disjoint iff the two sets in the family have empty intersection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( x = A -> C = D )   &    |- ( x = B -> C = E )   =>    |- ( ( A e. V /\ B e. V /\ A =/= B ) -> (Disj x e. { A , B } C <-> ( D i^i E ) = (/) ) )
Theorem	disjxiun 4649*	An indexed union of a disjoint collection of disjoint collections is disjoint if each component is disjoint, and the disjoint unions in the collection are also disjoint. Note that B ( y ) and C ( x ) may have the displayed free variables. (Contributed by Mario Carneiro, 14-Nov-2016.) (Proof shortened by JJ, 27-May-2021.)
|- (Disj y e. A B -> (Disj x e. U_ y e. A B C <-> ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) ) )
Theorem	disjxiunOLD 4650*	Obsolete proof of disjxiun 4649 as of 27-May-2021. An indexed union of a disjoint collection of disjoint collections is disjoint if each component is disjoint, and the disjoint unions in the collection are also disjoint. Note that B ( y ) and C ( x ) may have the displayed free variables. (Contributed by Mario Carneiro, 14-Nov-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- (Disj y e. A B -> (Disj x e. U_ y e. A B C <-> ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) ) )
Theorem	disjxun 4651*	The union of two disjoint collections. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( x = y -> C = D )   =>    |- ( ( A i^i B ) = (/) -> (Disj x e. ( A u. B ) C <-> (Disj x e. A C /\ Disj x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) ) )
Theorem	disjss3 4652*	Expand a disjoint collection with any number of empty sets. (Contributed by Mario Carneiro, 15-Nov-2016.)
|- ( ( A C_ B /\ A. x e. ( B \ A ) C = (/) ) -> (Disj x e. A C <-> Disj x e. B C ) )
2.1.22  Binary relations
Syntax	wbr 4653	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. (For an example of how syntax could become ambiguous if we are not careful, see the comment in cneg 10267.)
wff A R B
Definition	df-br 4654	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 R often denotes a relation such as " < " that compares two classes A and B, which might be numbers such as 1 and 2 (see df-ltxr 10079 for the specific definition of <). As a wff, relations are true or false. For example, ( R = { <. 2 , 6 >. , <. 3 , 9 >. } -> 3 R 9 ) (ex-br 27288). Often class R meets the Rel criteria to be defined in df-rel 5121, and in particular R may be a function (see df-fun 5890). This definition of relations is well-defined, although not very meaningful, when classes A and/or B are proper classes (i.e. are not sets). On the other hand, we often find uses for this definition when R is a proper class (see for example iprc 7101). (Contributed by NM, 31-Dec-1993.)
|- ( A R B <-> <. A , B >. e. R )
Theorem	breq 4655	Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.)
|- ( R = S -> ( A R B <-> A S B ) )
Theorem	breq1 4656	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
|- ( A = B -> ( A R C <-> B R C ) )
Theorem	breq2 4657	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
|- ( A = B -> ( C R A <-> C R B ) )
Theorem	breq12 4658	Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ( ( A = B /\ C = D ) -> ( A R C <-> B R D ) )
Theorem	breqi 4659	Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.)
|- R = S   =>    |- ( A R B <-> A S B )
Theorem	breq1i 4660	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- A = B   =>    |- ( A R C <-> B R C )
Theorem	breq2i 4661	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- A = B   =>    |- ( C R A <-> C R B )
Theorem	breq12i 4662	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|- A = B   &    |- C = D   =>    |- ( A R C <-> B R D )
Theorem	breq1d 4663	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A R C <-> B R C ) )
Theorem	breqd 4664	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C A D <-> C B D ) )
Theorem	breq2d 4665	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C R A <-> C R B ) )
Theorem	breq12d 4666	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A R C <-> B R D ) )
Theorem	breq123d 4667	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
|- ( ph -> A = B )   &    |- ( ph -> R = S )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A R C <-> B S D ) )
Theorem	breqdi 4668	Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 5-Oct-2020.)
|- ( ph -> A = B )   &    |- ( ph -> C A D )   =>    |- ( ph -> C B D )
Theorem	breqan12d 4669	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ( ph -> A = B )   &    |- ( ps -> C = D )   =>    |- ( ( ph /\ ps ) -> ( A R C <-> B R D ) )
Theorem	breqan12rd 4670	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ( ph -> A = B )   &    |- ( ps -> C = D )   =>    |- ( ( ps /\ ph ) -> ( A R C <-> B R D ) )
Theorem	eqnbrtrd 4671	Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> A = B )   &    |- ( ph -> -. B R C )   =>    |- ( ph -> -. A R C )
Theorem	nbrne1 4672	Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
|- ( ( A R B /\ -. A R C ) -> B =/= C )
Theorem	nbrne2 4673	Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
|- ( ( A R C /\ -. B R C ) -> A =/= B )
Theorem	eqbrtri 4674	Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
|- A = B   &    |- B R C   =>    |- A R C
Theorem	eqbrtrd 4675	Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)
|- ( ph -> A = B )   &    |- ( ph -> B R C )   =>    |- ( ph -> A R C )
Theorem	eqbrtrri 4676	Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
|- A = B   &    |- A R C   =>    |- B R C
Theorem	eqbrtrrd 4677	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
|- ( ph -> A = B )   &    |- ( ph -> A R C )   =>    |- ( ph -> B R C )
Theorem	breqtri 4678	Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
|- A R B   &    |- B = C   =>    |- A R C
Theorem	breqtrd 4679	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
|- ( ph -> A R B )   &    |- ( ph -> B = C )   =>    |- ( ph -> A R C )
Theorem	breqtrri 4680	Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
|- A R B   &    |- C = B   =>    |- A R C
Theorem	breqtrrd 4681	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
|- ( ph -> A R B )   &    |- ( ph -> C = B )   =>    |- ( ph -> A R C )
Theorem	3brtr3i 4682	Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
|- A R B   &    |- A = C   &    |- B = D   =>    |- C R D
Theorem	3brtr4i 4683	Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
|- A R B   &    |- C = A   &    |- D = B   =>    |- C R D
Theorem	3brtr3d 4684	Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)
|- ( ph -> A R B )   &    |- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> C R D )
Theorem	3brtr4d 4685	Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)
|- ( ph -> A R B )   &    |- ( ph -> C = A )   &    |- ( ph -> D = B )   =>    |- ( ph -> C R D )
Theorem	3brtr3g 4686	Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
|- ( ph -> A R B )   &    |- A = C   &    |- B = D   =>    |- ( ph -> C R D )
Theorem	3brtr4g 4687	Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
|- ( ph -> A R B )   &    |- C = A   &    |- D = B   =>    |- ( ph -> C R D )
Theorem	syl5eqbr 4688	A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
|- A = B   &    |- ( ph -> B R C )   =>    |- ( ph -> A R C )
Theorem	syl5eqbrr 4689	A chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.)
|- B = A   &    |- ( ph -> B R C )   =>    |- ( ph -> A R C )
Theorem	syl5breq 4690	A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
|- A R B   &    |- ( ph -> B = C )   =>    |- ( ph -> A R C )
Theorem	syl5breqr 4691	A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
|- A R B   &    |- ( ph -> C = B )   =>    |- ( ph -> A R C )
Theorem	syl6eqbr 4692	A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.)
|- ( ph -> A = B )   &    |- B R C   =>    |- ( ph -> A R C )
Theorem	syl6eqbrr 4693	A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> B = A )   &    |- B R C   =>    |- ( ph -> A R C )
Theorem	syl6breq 4694	A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
|- ( ph -> A R B )   &    |- B = C   =>    |- ( ph -> A R C )
Theorem	syl6breqr 4695	A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
|- ( ph -> A R B )   &    |- C = B   =>    |- ( ph -> A R C )
Theorem	ssbrd 4696	Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.)
|- ( ph -> A C_ B )   =>    |- ( ph -> ( C A D -> C B D ) )
Theorem	ssbri 4697	Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.)
|- A C_ B   =>    |- ( C A D -> C B D )
Theorem	nfbrd 4698	Deduction version of bound-variable hypothesis builder nfbr 4699. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x R )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/ x A R B )
Theorem	nfbr 4699	Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ x A   &    |- F/_ x R   &    |- F/_ x B   =>    |- F/ x A R B
Theorem	brab1 4700*	Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.)
|- ( x R A <-> x e. { z | z R A } )