P. 46 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4501-4600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	brab2ga 4501*	The law of concretion for a binary relation. See brab2a 4479 for alternate proof. TODO: should one of them be deleted? (Contributed by Mario Carneiro, 28-Apr-2015.) (Proof modification is discouraged.)
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )   &    |- R = { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ph ) }   =>    |- ( A R B <-> ( ( A e. C /\ B e. D ) /\ ps ) )
Theorem	optocl 4502*	Implicit substitution of class for ordered pair. (Contributed by NM, 5-Mar-1995.)
|- D = ( B X. C )   &    |- ( <. x , y >. = A -> ( ph <-> ps ) )   &    |- ( ( x e. B /\ y e. C ) -> ph )   =>    |- ( A e. D -> ps )
Theorem	2optocl 4503*	Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
|- R = ( C X. D )   &    |- ( <. x , y >. = A -> ( ph <-> ps ) )   &    |- ( <. z , w >. = B -> ( ps <-> ch ) )   &    |- ( ( ( x e. C /\ y e. D ) /\ ( z e. C /\ w e. D ) ) -> ph )   =>    |- ( ( A e. R /\ B e. R ) -> ch )
Theorem	3optocl 4504*	Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
|- R = ( D X. F )   &    |- ( <. x , y >. = A -> ( ph <-> ps ) )   &    |- ( <. z , w >. = B -> ( ps <-> ch ) )   &    |- ( <. v , u >. = C -> ( ch <-> th ) )   &    |- ( ( ( x e. D /\ y e. F ) /\ ( z e. D /\ w e. F ) /\ ( v e. D /\ u e. F ) ) -> ph )   =>    |- ( ( A e. R /\ B e. R /\ C e. R ) -> th )
Theorem	opbrop 4505*	Ordered pair membership in a relation. Special case. (Contributed by NM, 5-Aug-1995.)
|- ( ( ( z = A /\ w = B ) /\ ( v = C /\ u = D ) ) -> ( ph <-> ps ) )   &    |- R = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ph ) ) }   =>    |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <. A , B >. R <. C , D >. <-> ps ) )
Theorem	0xp 4506	The cross product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by NM, 4-Jul-1994.)
|- ( (/) X. A ) = (/)
Theorem	csbxpg 4507	Distribute proper substitution through the cross product of two classes. (Contributed by Alan Sare, 10-Nov-2012.)
|- ( A e. D -> [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C ) )
Theorem	releq 4508	Equality theorem for the relation predicate. (Contributed by NM, 1-Aug-1994.)
|- ( A = B -> ( Rel A <-> Rel B ) )
Theorem	releqi 4509	Equality inference for the relation predicate. (Contributed by NM, 8-Dec-2006.)
|- A = B   =>    |- ( Rel A <-> Rel B )
Theorem	releqd 4510	Equality deduction for the relation predicate. (Contributed by NM, 8-Mar-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> ( Rel A <-> Rel B ) )
Theorem	nfrel 4511	Bound-variable hypothesis builder for a relation. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   =>    |- F/ x Rel A
Theorem	sbcrel 4512	Distribute proper substitution through a relation predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
|- ( A e. V -> ( [. A / x ]. Rel R <-> Rel [_ A / x ]_ R ) )
Theorem	relss 4513	Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58. (Contributed by NM, 15-Aug-1994.)
|- ( A C_ B -> ( Rel B -> Rel A ) )
Theorem	ssrel 4514*	A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( Rel A -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )
Theorem	eqrel 4515*	Extensionality principle for relations. Theorem 3.2(ii) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.)
|- ( ( Rel A /\ Rel B ) -> ( A = B <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) ) )
Theorem	ssrel2 4516*	A subclass relationship depends only on a relation's ordered pairs. This version of ssrel 4514 is restricted to the relation's domain. (Contributed by Thierry Arnoux, 25-Jan-2018.)
|- ( R C_ ( A X. B ) -> ( R C_ S <-> A. x e. A A. y e. B ( <. x , y >. e. R -> <. x , y >. e. S ) ) )
Theorem	relssi 4517*	Inference from subclass principle for relations. (Contributed by NM, 31-Mar-1998.)
|- Rel A   &    |- ( <. x , y >. e. A -> <. x , y >. e. B )   =>    |- A C_ B
Theorem	relssdv 4518*	Deduction from subclass principle for relations. (Contributed by NM, 11-Sep-2004.)
|- ( ph -> Rel A )   &    |- ( ph -> ( <. x , y >. e. A -> <. x , y >. e. B ) )   =>    |- ( ph -> A C_ B )
Theorem	eqrelriv 4519*	Inference from extensionality principle for relations. (Contributed by FL, 15-Oct-2012.)
|- ( <. x , y >. e. A <-> <. x , y >. e. B )   =>    |- ( ( Rel A /\ Rel B ) -> A = B )
Theorem	eqrelriiv 4520*	Inference from extensionality principle for relations. (Contributed by NM, 17-Mar-1995.)
|- Rel A   &    |- Rel B   &    |- ( <. x , y >. e. A <-> <. x , y >. e. B )   =>    |- A = B
Theorem	eqbrriv 4521*	Inference from extensionality principle for relations. (Contributed by NM, 12-Dec-2006.)
|- Rel A   &    |- Rel B   &    |- ( x A y <-> x B y )   =>    |- A = B
Theorem	eqrelrdv 4522*	Deduce equality of relations from equivalence of membership. (Contributed by Rodolfo Medina, 10-Oct-2010.)
|- Rel A   &    |- Rel B   &    |- ( ph -> ( <. x , y >. e. A <-> <. x , y >. e. B ) )   =>    |- ( ph -> A = B )
Theorem	eqbrrdv 4523*	Deduction from extensionality principle for relations. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- ( ph -> Rel A )   &    |- ( ph -> Rel B )   &    |- ( ph -> ( x A y <-> x B y ) )   =>    |- ( ph -> A = B )
Theorem	eqbrrdiv 4524*	Deduction from extensionality principle for relations. (Contributed by Rodolfo Medina, 10-Oct-2010.)
|- Rel A   &    |- Rel B   &    |- ( ph -> ( x A y <-> x B y ) )   =>    |- ( ph -> A = B )
Theorem	eqrelrdv2 4525*	A version of eqrelrdv 4522. (Contributed by Rodolfo Medina, 10-Oct-2010.)
|- ( ph -> ( <. x , y >. e. A <-> <. x , y >. e. B ) )   =>    |- ( ( ( Rel A /\ Rel B ) /\ ph ) -> A = B )
Theorem	ssrelrel 4526*	A subclass relationship determined by ordered triples. Use relrelss 4944 to express the antecedent in terms of the relation predicate. (Contributed by NM, 17-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( A C_ ( ( _V X. _V ) X. _V ) -> ( A C_ B <-> A. x A. y A. z ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) ) )
Theorem	eqrelrel 4527*	Extensionality principle for ordered triples, analogous to eqrel 4515. Use relrelss 4944 to express the antecedent in terms of the relation predicate. (Contributed by NM, 17-Dec-2008.)
|- ( ( A u. B ) C_ ( ( _V X. _V ) X. _V ) -> ( A = B <-> A. x A. y A. z ( <. <. x , y >. , z >. e. A <-> <. <. x , y >. , z >. e. B ) ) )
Theorem	elrel 4528*	A member of a relation is an ordered pair. (Contributed by NM, 17-Sep-2006.)
|- ( ( Rel R /\ A e. R ) -> E. x E. y A = <. x , y >. )
Theorem	relsng 4529	A singleton is a relation iff it is an ordered pair. (Contributed by NM, 24-Sep-2013.) (Revised by BJ, 12-Feb-2022.)
|- ( A e. V -> ( Rel { A } <-> A e. ( _V X. _V ) ) )
Theorem	relsnopg 4530	A singleton of an ordered pair is a relation. (Contributed by NM, 17-May-1998.) (Revised by BJ, 12-Feb-2022.)
|- ( ( A e. V /\ B e. W ) -> Rel { <. A , B >. } )
Theorem	relsn 4531	A singleton is a relation iff it is an ordered pair. (Contributed by NM, 24-Sep-2013.)
|- A e. _V   =>    |- ( Rel { A } <-> A e. ( _V X. _V ) )
Theorem	relsnop 4532	A singleton of an ordered pair is a relation. (Contributed by NM, 17-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- A e. _V   &    |- B e. _V   =>    |- Rel { <. A , B >. }
Theorem	xpss12 4533	Subset theorem for cross product. Generalization of Theorem 101 of [Suppes] p. 52. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ( A C_ B /\ C C_ D ) -> ( A X. C ) C_ ( B X. D ) )
Theorem	xpss 4534	A cross product is included in the ordered pair universe. Exercise 3 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.)
|- ( A X. B ) C_ ( _V X. _V )
Theorem	relxp 4535	A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37. (Contributed by NM, 2-Aug-1994.)
|- Rel ( A X. B )
Theorem	xpss1 4536	Subset relation for cross product. (Contributed by Jeff Hankins, 30-Aug-2009.)
|- ( A C_ B -> ( A X. C ) C_ ( B X. C ) )
Theorem	xpss2 4537	Subset relation for cross product. (Contributed by Jeff Hankins, 30-Aug-2009.)
|- ( A C_ B -> ( C X. A ) C_ ( C X. B ) )
Theorem	xpsspw 4538	A cross product is included in the power of the power of the union of its arguments. (Contributed by NM, 13-Sep-2006.)
|- ( A X. B ) C_ ~P ~P ( A u. B )
Theorem	unixpss 4539	The double class union of a cross product is included in the union of its arguments. (Contributed by NM, 16-Sep-2006.)
|- U. U. ( A X. B ) C_ ( A u. B )
Theorem	xpexg 4540	The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.)
|- ( ( A e. V /\ B e. W ) -> ( A X. B ) e. _V )
Theorem	xpex 4541	The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.)
|- A e. _V   &    |- B e. _V   =>    |- ( A X. B ) e. _V
Theorem	relun 4542	The union of two relations is a relation. Compare Exercise 5 of [TakeutiZaring] p. 25. (Contributed by NM, 12-Aug-1994.)
|- ( Rel ( A u. B ) <-> ( Rel A /\ Rel B ) )
Theorem	relin1 4543	The intersection with a relation is a relation. (Contributed by NM, 16-Aug-1994.)
|- ( Rel A -> Rel ( A i^i B ) )
Theorem	relin2 4544	The intersection with a relation is a relation. (Contributed by NM, 17-Jan-2006.)
|- ( Rel B -> Rel ( A i^i B ) )
Theorem	reldif 4545	A difference cutting down a relation is a relation. (Contributed by NM, 31-Mar-1998.)
|- ( Rel A -> Rel ( A \ B ) )
Theorem	reliun 4546	An indexed union is a relation iff each member of its indexed family is a relation. (Contributed by NM, 19-Dec-2008.)
|- ( Rel U_ x e. A B <-> A. x e. A Rel B )
Theorem	reliin 4547	An indexed intersection is a relation if at least one of the member of the indexed family is a relation. (Contributed by NM, 8-Mar-2014.)
|- ( E. x e. A Rel B -> Rel |^|_ x e. A B )
Theorem	reluni 4548*	The union of a class is a relation iff any member is a relation. Exercise 6 of [TakeutiZaring] p. 25 and its converse. (Contributed by NM, 13-Aug-2004.)
|- ( Rel U. A <-> A. x e. A Rel x )
Theorem	relint 4549*	The intersection of a class is a relation if at least one member is a relation. (Contributed by NM, 8-Mar-2014.)
|- ( E. x e. A Rel x -> Rel |^| A )
Theorem	rel0 4550	The empty set is a relation. (Contributed by NM, 26-Apr-1998.)
|- Rel (/)
Theorem	relopabi 4551	A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.)
|- A = { <. x , y >. | ph }   =>    |- Rel A
Theorem	relopab 4552	A class of ordered pairs is a relation. (Contributed by NM, 8-Mar-1995.) (Unnecessary distinct variable restrictions were removed by Alan Sare, 9-Jul-2013.) (Proof shortened by Mario Carneiro, 21-Dec-2013.)
|- Rel { <. x , y >. | ph }
Theorem	reli 4553	The identity relation is a relation. Part of Exercise 4.12(p) of [Mendelson] p. 235. (Contributed by NM, 26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)
|- Rel _I
Theorem	rele 4554	The membership relation is a relation. (Contributed by NM, 26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)
|- Rel _E
Theorem	opabid2 4555*	A relation expressed as an ordered pair abstraction. (Contributed by NM, 11-Dec-2006.)
|- ( Rel A -> { <. x , y >. | <. x , y >. e. A } = A )
Theorem	inopab 4556*	Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
|- ( { <. x , y >. | ph } i^i { <. x , y >. | ps } ) = { <. x , y >. | ( ph /\ ps ) }
Theorem	difopab 4557*	The difference of two ordered-pair abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015.)
|- ( { <. x , y >. | ph } \ { <. x , y >. | ps } ) = { <. x , y >. | ( ph /\ -. ps ) }
Theorem	inxp 4558	The intersection of two cross products. Exercise 9 of [TakeutiZaring] p. 25. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ( A X. B ) i^i ( C X. D ) ) = ( ( A i^i C ) X. ( B i^i D ) )
Theorem	xpindi 4559	Distributive law for cross product over intersection. Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
|- ( A X. ( B i^i C ) ) = ( ( A X. B ) i^i ( A X. C ) )
Theorem	xpindir 4560	Distributive law for cross product over intersection. Similar to Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
|- ( ( A i^i B ) X. C ) = ( ( A X. C ) i^i ( B X. C ) )
Theorem	xpiindim 4561*	Distributive law for cross product over indexed intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
|- ( E. y y e. A -> ( C X. |^|_ x e. A B ) = |^|_ x e. A ( C X. B ) )
Theorem	xpriindim 4562*	Distributive law for cross product over relativized indexed intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
|- ( E. y y e. A -> ( C X. ( D i^i |^|_ x e. A B ) ) = ( ( C X. D ) i^i |^|_ x e. A ( C X. B ) ) )
Theorem	eliunxp 4563*	Membership in a union of cross products. Analogue of elxp 4445 for nonconstant B ( x ). (Contributed by Mario Carneiro, 29-Dec-2014.)
|- ( C e. U_ x e. A ( { x } X. B ) <-> E. x E. y ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
Theorem	opeliunxp2 4564*	Membership in a union of cross products. (Contributed by Mario Carneiro, 14-Feb-2015.)
|- ( x = C -> B = E )   =>    |- ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) )
Theorem	raliunxp 4565*	Write a double restricted quantification as one universal quantifier. In this version of ralxp 4567, B ( y ) is not assumed to be constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( A. x e. U_ y e. A ( { y } X. B ) ph <-> A. y e. A A. z e. B ps )
Theorem	rexiunxp 4566*	Write a double restricted quantification as one universal quantifier. In this version of rexxp 4568, B ( y ) is not assumed to be constant. (Contributed by Mario Carneiro, 14-Feb-2015.)
|- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( E. x e. U_ y e. A ( { y } X. B ) ph <-> E. y e. A E. z e. B ps )
Theorem	ralxp 4567*	Universal quantification restricted to a cross product is equivalent to a double restricted quantification. The hypothesis specifies an implicit substitution. (Contributed by NM, 7-Feb-2004.) (Revised by Mario Carneiro, 29-Dec-2014.)
|- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( A. x e. ( A X. B ) ph <-> A. y e. A A. z e. B ps )
Theorem	rexxp 4568*	Existential quantification restricted to a cross product is equivalent to a double restricted quantification. (Contributed by NM, 11-Nov-1995.) (Revised by Mario Carneiro, 14-Feb-2015.)
|- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( E. x e. ( A X. B ) ph <-> E. y e. A E. z e. B ps )
Theorem	djussxp 4569*	Disjoint union is a subset of a cross product. (Contributed by Stefan O'Rear, 21-Nov-2014.)
|- U_ x e. A ( { x } X. B ) C_ ( A X. _V )
Theorem	ralxpf 4570*	Version of ralxp 4567 with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/ y ph   &    |- F/ z ph   &    |- F/ x ps   &    |- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( A. x e. ( A X. B ) ph <-> A. y e. A A. z e. B ps )
Theorem	rexxpf 4571*	Version of rexxp 4568 with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/ y ph   &    |- F/ z ph   &    |- F/ x ps   &    |- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( E. x e. ( A X. B ) ph <-> E. y e. A E. z e. B ps )
Theorem	iunxpf 4572*	Indexed union on a cross product is equals a double indexed union. The hypothesis specifies an implicit substitution. (Contributed by NM, 19-Dec-2008.)
|- F/_ y C   &    |- F/_ z C   &    |- F/_ x D   &    |- ( x = <. y , z >. -> C = D )   =>    |- U_ x e. ( A X. B ) C = U_ y e. A U_ z e. B D
Theorem	opabbi2dv 4573*	Deduce equality of a relation and an ordered-pair class builder. Compare abbi2dv 2206. (Contributed by NM, 24-Feb-2014.)
|- Rel A   &    |- ( ph -> ( <. x , y >. e. A <-> ps ) )   =>    |- ( ph -> A = { <. x , y >. | ps } )
Theorem	relop 4574*	A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this detail.)
|- A e. _V   &    |- B e. _V   =>    |- ( Rel <. A , B >. <-> E. x E. y ( A = { x } /\ B = { x , y } ) )
Theorem	ideqg 4575	For sets, the identity relation is the same as equality. (Contributed by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( B e. V -> ( A _I B <-> A = B ) )
Theorem	ideq 4576	For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995.)
|- B e. _V   =>    |- ( A _I B <-> A = B )
Theorem	ididg 4577	A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( A e. V -> A _I A )
Theorem	issetid 4578	Two ways of expressing set existence. (Contributed by NM, 16-Feb-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( A e. _V <-> A _I A )
Theorem	coss1 4579	Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
|- ( A C_ B -> ( A o. C ) C_ ( B o. C ) )
Theorem	coss2 4580	Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
|- ( A C_ B -> ( C o. A ) C_ ( C o. B ) )
Theorem	coeq1 4581	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
|- ( A = B -> ( A o. C ) = ( B o. C ) )
Theorem	coeq2 4582	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
|- ( A = B -> ( C o. A ) = ( C o. B ) )
Theorem	coeq1i 4583	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
|- A = B   =>    |- ( A o. C ) = ( B o. C )
Theorem	coeq2i 4584	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
|- A = B   =>    |- ( C o. A ) = ( C o. B )
Theorem	coeq1d 4585	Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A o. C ) = ( B o. C ) )
Theorem	coeq2d 4586	Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C o. A ) = ( C o. B ) )
Theorem	coeq12i 4587	Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.)
|- A = B   &    |- C = D   =>    |- ( A o. C ) = ( B o. D )
Theorem	coeq12d 4588	Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A o. C ) = ( B o. D ) )
Theorem	nfco 4589	Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( A o. B )
Theorem	elco 4590*	Elements of a composed relation. (Contributed by BJ, 10-Jul-2022.)
|- ( A e. ( R o. S ) <-> E. x E. y E. z ( A = <. x , z >. /\ ( x S y /\ y R z ) ) )
Theorem	brcog 4591*	Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015.)
|- ( ( A e. V /\ B e. W ) -> ( A ( C o. D ) B <-> E. x ( A D x /\ x C B ) ) )
Theorem	opelco2g 4592*	Ordered pair membership in a composition. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.)
|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. ( C o. D ) <-> E. x ( <. A , x >. e. D /\ <. x , B >. e. C ) ) )
Theorem	brcogw 4593	Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14-Jan-2018.)
|- ( ( ( A e. V /\ B e. W /\ X e. Z ) /\ ( A D X /\ X C B ) ) -> A ( C o. D ) B )
Theorem	eqbrrdva 4594*	Deduction from extensionality principle for relations, given an equivalence only on the relation's domain and range. (Contributed by Thierry Arnoux, 28-Nov-2017.)
|- ( ph -> A C_ ( C X. D ) )   &    |- ( ph -> B C_ ( C X. D ) )   &    |- ( ( ph /\ x e. C /\ y e. D ) -> ( x A y <-> x B y ) )   =>    |- ( ph -> A = B )
Theorem	brco 4595*	Binary relation on a composition. (Contributed by NM, 21-Sep-2004.) (Revised by Mario Carneiro, 24-Feb-2015.)
|- A e. _V   &    |- B e. _V   =>    |- ( A ( C o. D ) B <-> E. x ( A D x /\ x C B ) )
Theorem	opelco 4596*	Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.)
|- A e. _V   &    |- B e. _V   =>    |- ( <. A , B >. e. ( C o. D ) <-> E. x ( A D x /\ x C B ) )
Theorem	cnvss 4597	Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
|- ( A C_ B -> `' A C_ `' B )
Theorem	cnveq 4598	Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)
|- ( A = B -> `' A = `' B )
Theorem	cnveqi 4599	Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
|- A = B   =>    |- `' A = `' B
Theorem	cnveqd 4600	Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)
|- ( ph -> A = B )   =>    |- ( ph -> `' A = `' B )