P. 47 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 4601-4700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	proj1op 4601	The first projection operator applied to an ordered pair yields its first member. Theorem X.2.7 of [Rosser] p. 282. (Contributed by SF, 3-Feb-2015.)
|- Proj1 <.A, B>. = A
Theorem	proj2op 4602	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 <.A, B>. = B
Theorem	opth 4603	The ordered pair theorem. Two ordered pairs are equal iff their components are equal. (Contributed by SF, 2-Jan-2015.)
|- (<.A, B>. = <.C, D>. <-> (A = C /\ B = D))
Theorem	opexb 4604	An ordered pair is a set iff its components are sets. (Contributed by SF, 2-Jan-2015.)
|- (<.A, B>. e. _V <-> (A e. _V /\ B e. _V))
Theorem	nfop 4605	Bound-variable hypothesis builder for ordered pairs. (Contributed by SF, 2-Jan-2015.)
|- F/_xA   &   |- F/_xB   =>   |- F/_x<.A, B>.
Theorem	nfopd 4606	Deduction version of bound-variable hypothesis builder nfop 4605. (Contributed by SF, 2-Jan-2015.)
|- (ph -> F/_xA)   &   |- (ph -> F/_xB)   =>   |- (ph -> F/_x<.A, B>.)
Theorem	eqvinop 4607*	A variable introduction law for ordered pairs. Analog of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.)
|- B e. _V   &   |- C e. _V   =>   |- (A = <.B, C>. <-> E.xE.y(A = <.x, y>. /\ <.x, y>. = <.B, C>.))
Theorem	copsexg 4608*	Substitution of class A for ordered pair <.x, y>.. (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 25-Jul-2011.)
|- (A = <.x, y>. -> (ph <-> E.xE.y(A = <.x, y>. /\ ph)))
Theorem	copsex2t 4609*	Closed theorem form of copsex2g 4610. (Contributed by NM, 17-Feb-2013.)
|- ((A.xA.y((x = A /\ y = B) -> (ph <-> ps)) /\ (A e. V /\ B e. W)) -> (E.xE.y(<.A, B>. = <.x, y>. /\ ph) <-> ps))
Theorem	copsex2g 4610*	Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.)
|- ((x = A /\ y = B) -> (ph <-> ps))   =>   |- ((A e. V /\ B e. W) -> (E.xE.y(<.A, B>. = <.x, y>. /\ ph) <-> ps))
Theorem	copsex4g 4611*	An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.)
|- (((x = A /\ y = B) /\ (z = C /\ w = D)) -> (ph <-> ps))   =>   |- (((A e. R /\ B e. S) /\ (C e. R /\ D e. S)) -> (E.xE.yE.zE.w((<.A, B>. = <.x, y>. /\ <.C, D>. = <.z, w>.) /\ ph) <-> ps))
Theorem	eqop 4612*	Express equality to an ordered pair. (Contributed by SF, 6-Jan-2015.)
|- (A = <.B, C>. <-> A.z(z e. A <-> (E.t e. B z = Phi t \/ E.t e. C z = ( Phi t u. {0c}))))
Theorem	mosubopt 4613*	"At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-Aug-2007.)
|- (A.yA.zE*xph -> E*xE.yE.z(A = <.y, z>. /\ ph))
Theorem	mosubop 4614*	"At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-May-1995.)
|- E*xph   =>   |- E*xE.yE.z(A = <.y, z>. /\ ph)
Theorem	phiun 4615	The phi operation distributes over union. (Contributed by SF, 20-Feb-2015.)
|- Phi (A u. B) = ( Phi A u. Phi B)
Theorem	phidisjnn 4616	The phi operation applied to a set disjoint from the naturals has no effect. (Contributed by SF, 20-Feb-2015.)
|- ((A i^i Nn ) = (/) -> Phi A = A)
Theorem	phialllem1 4617*	Lemma for phiall 4619. Any set of numbers without zero is the Phi of a set. (Contributed by Scott Fenton, 14-Apr-2021.)
|- A e. _V   =>   |- ((A C_ Nn /\ -. 0c e. A) -> E.x A = Phi x)
Theorem	phialllem2 4618*	Lemma for phiall 4619. Any set without 0c is equal to the Phi of a set. (Contributed by Scott Fenton, 8-Apr-2021.)
|- A e. _V   =>   |- (-. 0c e. A -> E.x A = Phi x)
Theorem	phiall 4619*	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.)
|- A e. _V   =>   |- E.x(A = Phi x \/ A = ( Phi x u. {0c}))
Theorem	opeq 4620	Any class is equal to an ordered pair. (Contributed by Scott Fenton, 8-Apr-2021.)
|- A = <. Proj1 A, Proj2 A>.
Theorem	opeqexb 4621*	A class is a set iff it is equal to an ordered pair. (Contributed by Scott Fenton, 19-Apr-2021.)
|- (A e. _V <-> E.xE.y A = <.x, y>.)
Theorem	opeqex 4622*	Any set is equal to some ordered pair. (Contributed by Scott Fenton, 16-Apr-2021.)
|- (A e. V -> E.xE.y A = <.x, y>.)
2.3.2  Ordered-pair class abstractions (class builders)
Syntax	copab 4623	Extend class notation to include ordered-pair class abstraction (class builder).
class {<.x, y>. | ph}
Definition	df-opab 4624*	Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually x and y are distinct, although the definition doesn't strictly require it (see dfid2 4770 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.)
|- {<.x, y>. | ph} = {z | E.xE.y(z = <.x, y>. /\ ph)}
Theorem	opabbid 4625	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.)
|- F/xph   &   |- F/yph   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> {<.x, y>. | ps} = {<.x, y>. | ch})
Theorem	opabbidv 4626*	Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (Contributed by NM, 15-May-1995.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> {<.x, y>. | ps} = {<.x, y>. | ch})
Theorem	opabbii 4627	Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
|- (ph <-> ps)   =>   |- {<.x, y>. | ph} = {<.x, y>. | ps}
Theorem	nfopab 4628*	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.)
|- F/zph   =>   |- F/_z{<.x, y>. | ph}
Theorem	nfopab1 4629	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.)
|- F/_x{<.x, y>. | ph}
Theorem	nfopab2 4630	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.)
|- F/_y{<.x, y>. | ph}
Theorem	cbvopab 4631*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.)
|- F/zph   &   |- F/wph   &   |- F/xps   &   |- F/yps   &   |- ((x = z /\ y = w) -> (ph <-> ps))   =>   |- {<.x, y>. | ph} = {<.z, w>. | ps}
Theorem	cbvopabv 4632*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.)
|- ((x = z /\ y = w) -> (ph <-> ps))   =>   |- {<.x, y>. | ph} = {<.z, w>. | ps}
Theorem	cbvopab1 4633*	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.)
|- F/zph   &   |- F/xps   &   |- (x = z -> (ph <-> ps))   =>   |- {<.x, y>. | ph} = {<.z, y>. | ps}
Theorem	cbvopab2 4634*	Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.)
|- F/zph   &   |- F/yps   &   |- (y = z -> (ph <-> ps))   =>   |- {<.x, y>. | ph} = {<.x, z>. | ps}
Theorem	cbvopab1s 4635*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.)
|- {<.x, y>. | ph} = {<.z, y>. | [z / x]ph}
Theorem	cbvopab1v 4636*	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.)
|- (x = z -> (ph <-> ps))   =>   |- {<.x, y>. | ph} = {<.z, y>. | ps}
Theorem	cbvopab2v 4637*	Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.)
|- (y = z -> (ph <-> ps))   =>   |- {<.x, y>. | ph} = {<.x, z>. | ps}
Theorem	csbopabg 4638*	Move substitution into a class abstraction. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|- (A e. V -> [_A / x]_{<.y, z>. | ph} = {<.y, z>. | [.A / x ].ph})
Theorem	unopab 4639	Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
|- ({<.x, y>. | ph} u. {<.x, y>. | ps}) = {<.x, y>. | (ph \/ ps)}
2.3.3  Binary relations
Syntax	wbr 4640	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.
wff ARB
Definition	df-br 4641	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 normally denotes a relation that compares two classes A and B. This definition 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. (Contributed by NM, 4-Jun-1995.)
|- (ARB <-> <.A, B>. e. R)
Theorem	breq 4642	Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.)
|- (R = S -> (ARB <-> ASB))
Theorem	breq1 4643	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
|- (A = B -> (ARC <-> BRC))
Theorem	breq2 4644	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
|- (A = B -> (CRA <-> CRB))
Theorem	breq12 4645	Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ((A = B /\ C = D) -> (ARC <-> BRD))
Theorem	breqi 4646	Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.)
|- R = S   =>   |- (ARB <-> ASB)
Theorem	breq1i 4647	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- A = B   =>   |- (ARC <-> BRC)
Theorem	breq2i 4648	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- A = B   =>   |- (CRA <-> CRB)
Theorem	breq12i 4649	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Revised by Eric Schmidt, 4-Apr-2007.)
|- A = B   &   |- C = D   =>   |- (ARC <-> BRD)
Theorem	breq1d 4650	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- (ph -> A = B)   =>   |- (ph -> (ARC <-> BRC))
Theorem	breqd 4651	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
|- (ph -> A = B)   =>   |- (ph -> (CAD <-> CBD))
Theorem	breq2d 4652	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- (ph -> A = B)   =>   |- (ph -> (CRA <-> CRB))
Theorem	breq12d 4653	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.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (ARC <-> BRD))
Theorem	breq123d 4654	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
|- (ph -> A = B)   &   |- (ph -> R = S)   &   |- (ph -> C = D)   =>   |- (ph -> (ARC <-> BSD))
Theorem	breqan12d 4655	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- (ph -> A = B)   &   |- (ps -> C = D)   =>   |- ((ph /\ ps) -> (ARC <-> BRD))
Theorem	breqan12rd 4656	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- (ph -> A = B)   &   |- (ps -> C = D)   =>   |- ((ps /\ ph) -> (ARC <-> BRD))
Theorem	nbrne1 4657	Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
|- ((ARB /\ -. ARC) -> B =/= C)
Theorem	nbrne2 4658	Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
|- ((ARC /\ -. BRC) -> A =/= B)
Theorem	eqbrtri 4659	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &   |- BRC   =>   |- ARC
Theorem	eqbrtrd 4660	Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)
|- (ph -> A = B)   &   |- (ph -> BRC)   =>   |- (ph -> ARC)
Theorem	eqbrtrri 4661	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &   |- ARC   =>   |- BRC
Theorem	eqbrtrrd 4662	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
|- (ph -> A = B)   &   |- (ph -> ARC)   =>   |- (ph -> BRC)
Theorem	breqtri 4663	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
|- ARB   &   |- B = C   =>   |- ARC
Theorem	breqtrd 4664	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
|- (ph -> ARB)   &   |- (ph -> B = C)   =>   |- (ph -> ARC)
Theorem	breqtrri 4665	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
|- ARB   &   |- C = B   =>   |- ARC
Theorem	breqtrrd 4666	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
|- (ph -> ARB)   &   |- (ph -> C = B)   =>   |- (ph -> ARC)
Theorem	3brtr3i 4667	Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
|- ARB   &   |- A = C   &   |- B = D   =>   |- CRD
Theorem	3brtr4i 4668	Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
|- ARB   &   |- C = A   &   |- D = B   =>   |- CRD
Theorem	3brtr3d 4669	Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)
|- (ph -> ARB)   &   |- (ph -> A = C)   &   |- (ph -> B = D)   =>   |- (ph -> CRD)
Theorem	3brtr4d 4670	Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)
|- (ph -> ARB)   &   |- (ph -> C = A)   &   |- (ph -> D = B)   =>   |- (ph -> CRD)
Theorem	3brtr3g 4671	Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
|- (ph -> ARB)   &   |- A = C   &   |- B = D   =>   |- (ph -> CRD)
Theorem	3brtr4g 4672	Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
|- (ph -> ARB)   &   |- C = A   &   |- D = B   =>   |- (ph -> CRD)
Theorem	syl5eqbr 4673	B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
|- A = B   &   |- (ph -> BRC)   =>   |- (ph -> ARC)
Theorem	syl5eqbrr 4674	B chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.)
|- B = A   &   |- (ph -> BRC)   =>   |- (ph -> ARC)
Theorem	syl5breq 4675	B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
|- ARB   &   |- (ph -> B = C)   =>   |- (ph -> ARC)
Theorem	syl5breqr 4676	B chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
|- ARB   &   |- (ph -> C = B)   =>   |- (ph -> ARC)
Theorem	syl6eqbr 4677	A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.)
|- (ph -> A = B)   &   |- BRC   =>   |- (ph -> ARC)
Theorem	syl6eqbrr 4678	A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.)
|- (ph -> B = A)   &   |- BRC   =>   |- (ph -> ARC)
Theorem	syl6breq 4679	A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
|- (ph -> ARB)   &   |- B = C   =>   |- (ph -> ARC)
Theorem	syl6breqr 4680	A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
|- (ph -> ARB)   &   |- C = B   =>   |- (ph -> ARC)
Theorem	ssbrd 4681	Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.)
|- (ph -> A C_ B)   =>   |- (ph -> (CAD -> CBD))
Theorem	ssbri 4682	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.)
|- A C_ B   =>   |- (CAD -> CBD)
Theorem	nfbrd 4683	Deduction version of bound-variable hypothesis builder nfbr 4684. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- (ph -> F/_xA)   &   |- (ph -> F/_xR)   &   |- (ph -> F/_xB)   =>   |- (ph -> F/x ARB)
Theorem	nfbr 4684	Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_xA   &   |- F/_xR   &   |- F/_xB   =>   |- F/x ARB
Theorem	brab1 4685*	Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.)
|- (xRA <-> x e. {z | zRA})
Theorem	sbcbrg 4686	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- (A e. D -> ( [.A / x ].BRC <-> [_A / x]_B[_A / x]_R[_A / x]_C))
Theorem	sbcbr12g 4687*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
|- (A e. D -> ( [.A / x ].BRC <-> [_A / x]_BR[_A / x]_C))
Theorem	sbcbr1g 4688*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
|- (A e. D -> ( [.A / x ].BRC <-> [_A / x]_BRC))
Theorem	sbcbr2g 4689*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
|- (A e. D -> ( [.A / x ].BRC <-> BR[_A / x]_C))
Theorem	brex 4690	Binary relationship implies sethood of both parts. (Contributed by SF, 7-Jan-2015.)
|- (ARB -> (A e. _V /\ B e. _V))
Theorem	brreldmex 4691	Binary relationship implies sethood of domain. (Contributed by SF, 7-Jan-2018.)
|- (ARB -> A e. _V)
Theorem	brrelrnex 4692	Binary relationship implies sethood of range. (Contributed by SF, 7-Jan-2018.)
|- (ARB -> B e. _V)
Theorem	brun 4693	The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
|- (A(R u. S)B <-> (ARB \/ ASB))
Theorem	brin 4694	The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
|- (A(R i^i S)B <-> (ARB /\ ASB))
Theorem	brdif 4695	The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.)
|- (A(R \ S)B <-> (ARB /\ -. ASB))
2.3.4  Ordered-pair class abstractions (cont.)
Theorem	opabid 4696	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.)
|- (<.x, y>. e. {<.x, y>. | ph} <-> ph)
Theorem	elopab 4697*	Membership in a class abstraction of pairs. (Contributed by NM, 24-Mar-1998.)
|- (A e. {<.x, y>. | ph} <-> E.xE.y(A = <.x, y>. /\ ph))
Theorem	opelopabsb 4698*	The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
|- (<.A, B>. e. {<.x, y>. | ph} <-> [.A / x ]. [.B / y ].ph)
Theorem	brabsb 4699*	The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.)
|- R = {<.x, y>. | ph}   =>   |- (ARB <-> [.A / x ]. [.B / y ].ph)
Theorem	opelopabt 4700*	Closed theorem form of opelopab 4709. (Contributed by NM, 19-Feb-2013.)
|- ((A.xA.y(x = A -> (ph <-> ps)) /\ A.xA.y(y = B -> (ps <-> ch)) /\ (A e. V /\ B e. W)) -> (<.A, B>. e. {<.x, y>. | ph} <-> ch))