P. 45 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4401-4500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfop 4401	Value of an ordered pair when the arguments are sets, with the conclusion corresponding to Kuratowski's original definition. (Contributed by NM, 25-Jun-1998.) (Avoid depending on this detail.)
|- A e. _V   &    |- B e. _V   =>    |- <. A , B >. = { { A } , { A , B } }
Theorem	opeq1 4402	Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( A = B -> <. A , C >. = <. B , C >. )
Theorem	opeq2 4403	Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( A = B -> <. C , A >. = <. C , B >. )
Theorem	opeq12 4404	Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)
|- ( ( A = C /\ B = D ) -> <. A , B >. = <. C , D >. )
Theorem	opeq1i 4405	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
|- A = B   =>    |- <. A , C >. = <. B , C >.
Theorem	opeq2i 4406	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
|- A = B   =>    |- <. C , A >. = <. C , B >.
Theorem	opeq12i 4407	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|- A = B   &    |- C = D   =>    |- <. A , C >. = <. B , D >.
Theorem	opeq1d 4408	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
|- ( ph -> A = B )   =>    |- ( ph -> <. A , C >. = <. B , C >. )
Theorem	opeq2d 4409	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
|- ( ph -> A = B )   =>    |- ( ph -> <. C , A >. = <. C , B >. )
Theorem	opeq12d 4410	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> <. A , C >. = <. B , D >. )
Theorem	oteq1 4411	Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|- ( A = B -> <. A , C , D >. = <. B , C , D >. )
Theorem	oteq2 4412	Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|- ( A = B -> <. C , A , D >. = <. C , B , D >. )
Theorem	oteq3 4413	Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|- ( A = B -> <. C , D , A >. = <. C , D , B >. )
Theorem	oteq1d 4414	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- ( ph -> A = B )   =>    |- ( ph -> <. A , C , D >. = <. B , C , D >. )
Theorem	oteq2d 4415	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- ( ph -> A = B )   =>    |- ( ph -> <. C , A , D >. = <. C , B , D >. )
Theorem	oteq3d 4416	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- ( ph -> A = B )   =>    |- ( ph -> <. C , D , A >. = <. C , D , B >. )
Theorem	oteq123d 4417	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   &    |- ( ph -> E = F )   =>    |- ( ph -> <. A , C , E >. = <. B , D , F >. )
Theorem	nfop 4418	Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x <. A , B >.
Theorem	nfopd 4419	Deduction version of bound-variable hypothesis builder nfop 4418. This shows how the deduction version of a not-free theorem such as nfop 4418 can be created from the corresponding not-free inference theorem. (Contributed by NM, 4-Feb-2008.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/_ x <. A , B >. )
Theorem	csbopg 4420	Distribution of class substitution over ordered pairs. (Contributed by Drahflow, 25-Sep-2015.) (Revised by Mario Carneiro, 29-Oct-2015.) (Revised by ML, 25-Oct-2020.)
|- ( A e. V -> [_ A / x ]_ <. C , D >. = <. [_ A / x ]_ C , [_ A / x ]_ D >. )
Theorem	opid 4421	The ordered pair <. A , A >. in Kuratowski's representation. (Contributed by FL, 28-Dec-2011.) (Avoid depending on this detail.)
|- A e. _V   =>    |- <. A , A >. = { { A } }
Theorem	ralunsn 4422*	Restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- ( x = B -> ( ph <-> ps ) )   =>    |- ( B e. C -> ( A. x e. ( A u. { B } ) ph <-> ( A. x e. A ph /\ ps ) ) )
Theorem	2ralunsn 4423*	Double restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.)
|- ( x = B -> ( ph <-> ch ) )   &    |- ( y = B -> ( ph <-> ps ) )   &    |- ( x = B -> ( ps <-> th ) )   =>    |- ( B e. C -> ( A. x e. ( A u. { B } ) A. y e. ( A u. { B } ) ph <-> ( ( A. x e. A A. y e. A ph /\ A. x e. A ps ) /\ ( A. y e. A ch /\ th ) ) ) )
Theorem	opprc 4424	Expansion of an ordered pair when either member is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( -. ( A e. _V /\ B e. _V ) -> <. A , B >. = (/) )
Theorem	opprc1 4425	Expansion of an ordered pair when the first member is a proper class. See also opprc 4424. (Contributed by NM, 10-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( -. A e. _V -> <. A , B >. = (/) )
Theorem	opprc2 4426	Expansion of an ordered pair when the second member is a proper class. See also opprc 4424. (Contributed by NM, 15-Nov-1994.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( -. B e. _V -> <. A , B >. = (/) )
Theorem	oprcl 4427	If an ordered pair has an element, then its arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( C e. <. A , B >. -> ( A e. _V /\ B e. _V ) )
Theorem	pwsn 4428	The power set of a singleton. (Contributed by NM, 5-Jun-2006.)
|- ~P { A } = { (/) , { A } }
Theorem	pwsnALT 4429	Alternate proof of pwsn 4428, more direct. (Contributed by NM, 5-Jun-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ~P { A } = { (/) , { A } }
Theorem	pwpr 4430	The power set of an unordered pair. (Contributed by NM, 1-May-2009.)
|- ~P { A , B } = ( { (/) , { A } } u. { { B } , { A , B } } )
Theorem	pwtp 4431	The power set of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016.)
|- ~P { A , B , C } = ( ( { (/) , { A } } u. { { B } , { A , B } } ) u. ( { { C } , { A , C } } u. { { B , C } , { A , B , C } } ) )
Theorem	pwpwpw0 4432	Compute the power set of the power set of the power set of the empty set. (See also pw0 4343 and pwpw0 4344.) (Contributed by NM, 2-May-2009.)
|- ~P { (/) , { (/) } } = ( { (/) , { (/) } } u. { { { (/) } } , { (/) , { (/) } } } )
Theorem	pwv 4433	The power class of the universe is the universe. Exercise 4.12(d) of [Mendelson] p. 235. (Contributed by NM, 14-Sep-2003.)
|- ~P _V = _V
Theorem	prproe 4434*	For an element of a proper unordered pair of elements of a class V, there is another (different) element of the class V which is an element of the proper pair. (Contributed by AV, 18-Dec-2021.)
|- ( ( C e. { A , B } /\ A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } )
Theorem	3elpr2eq 4435	If there are three elements in a proper unordered pair, and two of them are different from the third one, the two must be equal. (Contributed by AV, 19-Dec-2021.)
|- ( ( ( X e. { A , B } /\ Y e. { A , B } /\ Z e. { A , B } ) /\ ( Y =/= X /\ Z =/= X ) ) -> Y = Z )
2.1.18  The union of a class
Syntax	cuni 4436	Extend class notation to include the union of a class (read: 'union A')
class U. A
Definition	df-uni 4437*	Define the union of a class i.e. the collection of all members of the members of the class. Definition 5.5 of [TakeutiZaring] p. 16. For example, U. { { 1 , 3 } , { 1 , 8 } } = { 1 , 3 , 8 } (ex-uni 27283). This is similar to the union of two classes df-un 3579. (Contributed by NM, 23-Aug-1993.)
|- U. A = { x | E. y ( x e. y /\ y e. A ) }
Theorem	dfuni2 4438*	Alternate definition of class union. (Contributed by NM, 28-Jun-1998.)
|- U. A = { x | E. y e. A x e. y }
Theorem	eluni 4439*	Membership in class union. (Contributed by NM, 22-May-1994.)
|- ( A e. U. B <-> E. x ( A e. x /\ x e. B ) )
Theorem	eluni2 4440*	Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.)
|- ( A e. U. B <-> E. x e. B A e. x )
Theorem	elunii 4441	Membership in class union. (Contributed by NM, 24-Mar-1995.)
|- ( ( A e. B /\ B e. C ) -> A e. U. C )
Theorem	nfuni 4442	Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- F/_ x A   =>    |- F/_ x U. A
Theorem	nfunid 4443	Deduction version of nfuni 4442. (Contributed by NM, 18-Feb-2013.)
|- ( ph -> F/_ x A )   =>    |- ( ph -> F/_ x U. A )
Theorem	unieq 4444	Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18. (Contributed by NM, 10-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ( A = B -> U. A = U. B )
Theorem	unieqi 4445	Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.)
|- A = B   =>    |- U. A = U. B
Theorem	unieqd 4446	Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)
|- ( ph -> A = B )   =>    |- ( ph -> U. A = U. B )
Theorem	eluniab 4447*	Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.)
|- ( A e. U. { x | ph } <-> E. x ( A e. x /\ ph ) )
Theorem	elunirab 4448*	Membership in union of a class abstraction. (Contributed by NM, 4-Oct-2006.)
|- ( A e. U. { x e. B | ph } <-> E. x e. B ( A e. x /\ ph ) )
Theorem	unipr 4449	The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 23-Aug-1993.)
|- A e. _V   &    |- B e. _V   =>    |- U. { A , B } = ( A u. B )
Theorem	uniprg 4450	The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 25-Aug-2006.)
|- ( ( A e. V /\ B e. W ) -> U. { A , B } = ( A u. B ) )
Theorem	unisn 4451	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 30-Aug-1993.)
|- A e. _V   =>    |- U. { A } = A
Theorem	unisng 4452	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 13-Aug-2002.)
|- ( A e. V -> U. { A } = A )
Theorem	unisn3 4453*	Union of a singleton in the form of a restricted class abstraction. (Contributed by NM, 3-Jul-2008.)
|- ( A e. B -> U. { x e. B | x = A } = A )
Theorem	dfnfc2 4454*	An alternative statement of the effective freeness of a class A, when it is a set. (Contributed by Mario Carneiro, 14-Oct-2016.) (Proof shortened by JJ, 26-Jul-2021.)
|- ( A. x A e. V -> ( F/_ x A <-> A. y F/ x y = A ) )
Theorem	dfnfc2OLD 4455*	Obsolete proof of dfnfc2 4454 as of 26-Jul-2021. (Contributed by Mario Carneiro, 14-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x A e. V -> ( F/_ x A <-> A. y F/ x y = A ) )
Theorem	uniun 4456	The class union of the union of two classes. Theorem 8.3 of [Quine] p. 53. (Contributed by NM, 20-Aug-1993.)
|- U. ( A u. B ) = ( U. A u. U. B )
Theorem	uniin 4457	The class union of the intersection of two classes. Exercise 4.12(n) of [Mendelson] p. 235. See uniinqs 7827 for a condition where equality holds. (Contributed by NM, 4-Dec-2003.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- U. ( A i^i B ) C_ ( U. A i^i U. B )
Theorem	uniss 4458	Subclass relationship for class union. Theorem 61 of [Suppes] p. 39. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ( A C_ B -> U. A C_ U. B )
Theorem	ssuni 4459	Subclass relationship for class union. (Contributed by NM, 24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 26-Jul-2021.)
|- ( ( A C_ B /\ B e. C ) -> A C_ U. C )
Theorem	ssuniOLD 4460	Obsolete proof of ssuni 4459 as of 26-Jul-2021. (Contributed by NM, 24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( A C_ B /\ B e. C ) -> A C_ U. C )
Theorem	unissi 4461	Subclass relationship for subclass union. Inference form of uniss 4458. (Contributed by David Moews, 1-May-2017.)
|- A C_ B   =>    |- U. A C_ U. B
Theorem	unissd 4462	Subclass relationship for subclass union. Deduction form of uniss 4458. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A C_ B )   =>    |- ( ph -> U. A C_ U. B )
Theorem	uni0b 4463	The union of a set is empty iff the set is included in the singleton of the empty set. (Contributed by NM, 12-Sep-2004.)
|- ( U. A = (/) <-> A C_ { (/) } )
Theorem	uni0c 4464*	The union of a set is empty iff all of its members are empty. (Contributed by NM, 16-Aug-2006.)
|- ( U. A = (/) <-> A. x e. A x = (/) )
Theorem	uni0 4465	The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul 4789 by Eric Schmidt.) (Contributed by NM, 16-Sep-1993.) (Revised by Eric Schmidt, 4-Apr-2007.)
|- U. (/) = (/)
Theorem	csbuni 4466	Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012.) (Revised by NM, 22-Aug-2018.)
|- [_ A / x ]_ U. B = U. [_ A / x ]_ B
Theorem	elssuni 4467	An element of a class is a subclass of its union. Theorem 8.6 of [Quine] p. 54. Also the basis for Proposition 7.20 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Jun-1994.)
|- ( A e. B -> A C_ U. B )
Theorem	unissel 4468	Condition turning a subclass relationship for union into an equality. (Contributed by NM, 18-Jul-2006.)
|- ( ( U. A C_ B /\ B e. A ) -> U. A = B )
Theorem	unissb 4469*	Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.)
|- ( U. A C_ B <-> A. x e. A x C_ B )
Theorem	uniss2 4470*	A subclass condition on the members of two classes that implies a subclass relation on their unions. Proposition 8.6 of [TakeutiZaring] p. 59. See iunss2 4565 for a generalization to indexed unions. (Contributed by NM, 22-Mar-2004.)
|- ( A. x e. A E. y e. B x C_ y -> U. A C_ U. B )
Theorem	unidif 4471*	If the difference A \ B contains the largest members of A, then the union of the difference is the union of A. (Contributed by NM, 22-Mar-2004.)
|- ( A. x e. A E. y e. ( A \ B ) x C_ y -> U. ( A \ B ) = U. A )
Theorem	ssunieq 4472*	Relationship implying union. (Contributed by NM, 10-Nov-1999.)
|- ( ( A e. B /\ A. x e. B x C_ A ) -> A = U. B )
Theorem	unimax 4473*	Any member of a class is the largest of those members that it includes. (Contributed by NM, 13-Aug-2002.)
|- ( A e. B -> U. { x e. B | x C_ A } = A )
Theorem	pwuni 4474	A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.)
|- A C_ ~P U. A
2.1.19  The intersection of a class
Syntax	cint 4475	Extend class notation to include the intersection of a class (read: 'intersect A').
class |^| A
Definition	df-int 4476*	Define the intersection of a class. Definition 7.35 of [TakeutiZaring] p. 44. For example, |^| { { 1 , 3 } , { 1 , 8 } } = { 1 }. Compare this with the intersection of two classes, df-in 3581. (Contributed by NM, 18-Aug-1993.)
|- |^| A = { x | A. y ( y e. A -> x e. y ) }
Theorem	dfint2 4477*	Alternate definition of class intersection. (Contributed by NM, 28-Jun-1998.)
|- |^| A = { x | A. y e. A x e. y }
Theorem	inteq 4478	Equality law for intersection. (Contributed by NM, 13-Sep-1999.)
|- ( A = B -> |^| A = |^| B )
Theorem	inteqi 4479	Equality inference for class intersection. (Contributed by NM, 2-Sep-2003.)
|- A = B   =>    |- |^| A = |^| B
Theorem	inteqd 4480	Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.)
|- ( ph -> A = B )   =>    |- ( ph -> |^| A = |^| B )
Theorem	elint 4481*	Membership in class intersection. (Contributed by NM, 21-May-1994.)
|- A e. _V   =>    |- ( A e. |^| B <-> A. x ( x e. B -> A e. x ) )
Theorem	elint2 4482*	Membership in class intersection. (Contributed by NM, 14-Oct-1999.)
|- A e. _V   =>    |- ( A e. |^| B <-> A. x e. B A e. x )
Theorem	elintg 4483*	Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003.) (Proof shortened by JJ, 26-Jul-2021.)
|- ( A e. V -> ( A e. |^| B <-> A. x e. B A e. x ) )
Theorem	elintgOLD 4484*	Obsolete proof of elintg 4483 as of 26-Jul-2021. (Contributed by NM, 20-Nov-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A e. V -> ( A e. |^| B <-> A. x e. B A e. x ) )
Theorem	elinti 4485	Membership in class intersection. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( A e. |^| B -> ( C e. B -> A e. C ) )
Theorem	nfint 4486	Bound-variable hypothesis builder for intersection. (Contributed by NM, 2-Feb-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
|- F/_ x A   =>    |- F/_ x |^| A
Theorem	elintab 4487*	Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993.)
|- A e. _V   =>    |- ( A e. |^| { x | ph } <-> A. x ( ph -> A e. x ) )
Theorem	elintrab 4488*	Membership in the intersection of a class abstraction. (Contributed by NM, 17-Oct-1999.)
|- A e. _V   =>    |- ( A e. |^| { x e. B | ph } <-> A. x e. B ( ph -> A e. x ) )
Theorem	elintrabg 4489*	Membership in the intersection of a class abstraction. (Contributed by NM, 17-Feb-2007.)
|- ( A e. V -> ( A e. |^| { x e. B | ph } <-> A. x e. B ( ph -> A e. x ) ) )
Theorem	int0 4490	The intersection of the empty set is the universal class. Exercise 2 of [TakeutiZaring] p. 44. (Contributed by NM, 18-Aug-1993.) (Proof shortened by JJ, 26-Jul-2021.)
|- |^| (/) = _V
Theorem	int0OLD 4491	Obsolete proof of int0 4490 as of 26-Jul-2021. (Contributed by NM, 18-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- |^| (/) = _V
Theorem	intss1 4492	An element of a class includes the intersection of the class. Exercise 4 of [TakeutiZaring] p. 44 (with correction), generalized to classes. (Contributed by NM, 18-Nov-1995.)
|- ( A e. B -> |^| B C_ A )
Theorem	ssint 4493*	Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52 and its converse. (Contributed by NM, 14-Oct-1999.)
|- ( A C_ |^| B <-> A. x e. B A C_ x )
Theorem	ssintab 4494*	Subclass of the intersection of a class abstraction. (Contributed by NM, 31-Jul-2006.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( A C_ |^| { x | ph } <-> A. x ( ph -> A C_ x ) )
Theorem	ssintub 4495*	Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.)
|- A C_ |^| { x e. B | A C_ x }
Theorem	ssmin 4496*	Subclass of the minimum value of class of supersets. (Contributed by NM, 10-Aug-2006.)
|- A C_ |^| { x | ( A C_ x /\ ph ) }
Theorem	intmin 4497*	Any member of a class is the smallest of those members that include it. (Contributed by NM, 13-Aug-2002.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( A e. B -> |^| { x e. B | A C_ x } = A )
Theorem	intss 4498	Intersection of subclasses. (Contributed by NM, 14-Oct-1999.) (Proof shortened by OpenAI, 25-Mar-2020.)
|- ( A C_ B -> |^| B C_ |^| A )
Theorem	intssuni 4499	The intersection of a nonempty set is a subclass of its union. (Contributed by NM, 29-Jul-2006.)
|- ( A =/= (/) -> |^| A C_ U. A )
Theorem	ssintrab 4500*	Subclass of the intersection of a restricted class builder. (Contributed by NM, 30-Jan-2015.)
|- ( A C_ |^| { x e. B | ph } <-> A. x e. B ( ph -> A C_ x ) )