P. 38 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3701-3800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	preqr1g 3701	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. Closed form of preqr1 3703. (Contributed by Jim Kingdon, 21-Sep-2018.)
|- ( ( A e. _V /\ B e. _V ) -> ( { A , C } = { B , C } -> A = B ) )
Theorem	preqr2g 3702	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the second elements are equal. Closed form of preqr2 3704. (Contributed by Jim Kingdon, 21-Sep-2018.)
|- ( ( A e. _V /\ B e. _V ) -> ( { C , A } = { C , B } -> A = B ) )
Theorem	preqr1 3703	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. (Contributed by NM, 18-Oct-1995.)
|- A e. _V   &    |- B e. _V   =>    |- ( { A , C } = { B , C } -> A = B )
Theorem	preqr2 3704	Reverse equality lemma for unordered pairs. If two unordered pairs have the same first element, the second elements are equal. (Contributed by NM, 5-Aug-1993.)
|- A e. _V   &    |- B e. _V   =>    |- ( { C , A } = { C , B } -> A = B )
Theorem	preq12b 3705	Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   =>    |- ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) )
Theorem	prel12 3706	Equality of two unordered pairs. (Contributed by NM, 17-Oct-1996.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   =>    |- ( -. A = B -> ( { A , B } = { C , D } <-> ( A e. { C , D } /\ B e. { C , D } ) ) )
Theorem	opthpr 3707	A way to represent ordered pairs using unordered pairs with distinct members. (Contributed by NM, 27-Mar-2007.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   =>    |- ( A =/= D -> ( { A , B } = { C , D } <-> ( A = C /\ B = D ) ) )
Theorem	preq12bg 3708	Closed form of preq12b 3705. (Contributed by Scott Fenton, 28-Mar-2014.)
|- ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
Theorem	prneimg 3709	Two pairs are not equal if at least one element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
|- ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) ) -> ( ( ( A =/= C /\ A =/= D ) \/ ( B =/= C /\ B =/= D ) ) -> { A , B } =/= { C , D } ) )
Theorem	preqsn 3710	Equivalence for a pair equal to a singleton. (Contributed by NM, 3-Jun-2008.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( { A , B } = { C } <-> ( A = B /\ B = C ) )
Theorem	dfopg 3711	Value of the ordered pair when the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
Theorem	dfop 3712	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.)
|- A e. _V   &    |- B e. _V   =>    |- <. A , B >. = { { A } , { A , B } }
Theorem	opeq1 3713	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 3714	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 3715	Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)
|- ( ( A = C /\ B = D ) -> <. A , B >. = <. C , D >. )
Theorem	opeq1i 3716	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
|- A = B   =>    |- <. A , C >. = <. B , C >.
Theorem	opeq2i 3717	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
|- A = B   =>    |- <. C , A >. = <. C , B >.
Theorem	opeq12i 3718	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 3719	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
|- ( ph -> A = B )   =>    |- ( ph -> <. A , C >. = <. B , C >. )
Theorem	opeq2d 3720	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
|- ( ph -> A = B )   =>    |- ( ph -> <. C , A >. = <. C , B >. )
Theorem	opeq12d 3721	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 3722	Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|- ( A = B -> <. A , C , D >. = <. B , C , D >. )
Theorem	oteq2 3723	Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|- ( A = B -> <. C , A , D >. = <. C , B , D >. )
Theorem	oteq3 3724	Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|- ( A = B -> <. C , D , A >. = <. C , D , B >. )
Theorem	oteq1d 3725	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- ( ph -> A = B )   =>    |- ( ph -> <. A , C , D >. = <. B , C , D >. )
Theorem	oteq2d 3726	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- ( ph -> A = B )   =>    |- ( ph -> <. C , A , D >. = <. C , B , D >. )
Theorem	oteq3d 3727	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- ( ph -> A = B )   =>    |- ( ph -> <. C , D , A >. = <. C , D , B >. )
Theorem	oteq123d 3728	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 3729	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 3730	Deduction version of bound-variable hypothesis builder nfop 3729. This shows how the deduction version of a not-free theorem such as nfop 3729 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	opid 3731	The ordered pair <. A , A >. in Kuratowski's representation. (Contributed by FL, 28-Dec-2011.)
|- A e. _V   =>    |- <. A , A >. = { { A } }
Theorem	ralunsn 3732*	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 3733*	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 3734	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 3735	Expansion of an ordered pair when the first member is a proper class. See also opprc 3734. (Contributed by NM, 10-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( -. A e. _V -> <. A , B >. = (/) )
Theorem	opprc2 3736	Expansion of an ordered pair when the second member is a proper class. See also opprc 3734. (Contributed by NM, 15-Nov-1994.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( -. B e. _V -> <. A , B >. = (/) )
Theorem	oprcl 3737	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	pwsnss 3738	The power set of a singleton. (Contributed by Jim Kingdon, 12-Aug-2018.)
|- { (/) , { A } } C_ ~P { A }
Theorem	pwpw0ss 3739	Compute the power set of the power set of the empty set. (See pw0 3675 for the power set of the empty set.) Theorem 90 of [Suppes] p. 48 (but with subset in place of equality). (Contributed by Jim Kingdon, 12-Aug-2018.)
|- { (/) , { (/) } } C_ ~P { (/) }
Theorem	pwprss 3740	The power set of an unordered pair. (Contributed by Jim Kingdon, 13-Aug-2018.)
|- ( { (/) , { A } } u. { { B } , { A , B } } ) C_ ~P { A , B }
Theorem	pwtpss 3741	The power set of an unordered triple. (Contributed by Jim Kingdon, 13-Aug-2018.)
|- ( ( { (/) , { A } } u. { { B } , { A , B } } ) u. ( { { C } , { A , C } } u. { { B , C } , { A , B , C } } ) ) C_ ~P { A , B , C }
Theorem	pwpwpw0ss 3742	Compute the power set of the power set of the power set of the empty set. (See also pw0 3675 and pwpw0ss 3739.) (Contributed by Jim Kingdon, 13-Aug-2018.)
|- ( { (/) , { (/) } } u. { { { (/) } } , { (/) , { (/) } } } ) C_ ~P { (/) , { (/) } }
Theorem	pwv 3743	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
2.1.18  The union of a class
Syntax	cuni 3744	Extend class notation to include the union of a class (read: 'union A')
class U. A
Definition	df-uni 3745*	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, { { 1 , 3 } , { 1 , 8 } } = { 1 , 3 , 8 } . This is similar to the union of two classes df-un 3080. (Contributed by NM, 23-Aug-1993.)
|- U. A = { x | E. y ( x e. y /\ y e. A ) }
Theorem	dfuni2 3746*	Alternate definition of class union. (Contributed by NM, 28-Jun-1998.)
|- U. A = { x | E. y e. A x e. y }
Theorem	eluni 3747*	Membership in class union. (Contributed by NM, 22-May-1994.)
|- ( A e. U. B <-> E. x ( A e. x /\ x e. B ) )
Theorem	eluni2 3748*	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 3749	Membership in class union. (Contributed by NM, 24-Mar-1995.)
|- ( ( A e. B /\ B e. C ) -> A e. U. C )
Theorem	nfuni 3750	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 3751	Deduction version of nfuni 3750. (Contributed by NM, 18-Feb-2013.)
|- ( ph -> F/_ x A )   =>    |- ( ph -> F/_ x U. A )
Theorem	csbunig 3752	Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012.)
|- ( A e. V -> [_ A / x ]_ U. B = U. [_ A / x ]_ B )
Theorem	unieq 3753	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 3754	Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.)
|- A = B   =>    |- U. A = U. B
Theorem	unieqd 3755	Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)
|- ( ph -> A = B )   =>    |- ( ph -> U. A = U. B )
Theorem	eluniab 3756*	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 3757*	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 3758	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 3759	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 3760	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 3761	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	dfnfc2 3762*	An alternate statement of the effective freeness of a class A, when it is a set. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- ( A. x A e. V -> ( F/_ x A <-> A. y F/ x y = A ) )
Theorem	uniun 3763	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 3764	The class union of the intersection of two classes. Exercise 4.12(n) of [Mendelson] p. 235. (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 3765	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 3766	Subclass relationship for class union. (Contributed by NM, 24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ( ( A C_ B /\ B e. C ) -> A C_ U. C )
Theorem	unissi 3767	Subclass relationship for subclass union. Inference form of uniss 3765. (Contributed by David Moews, 1-May-2017.)
|- A C_ B   =>    |- U. A C_ U. B
Theorem	unissd 3768	Subclass relationship for subclass union. Deduction form of uniss 3765. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A C_ B )   =>    |- ( ph -> U. A C_ U. B )
Theorem	uni0b 3769	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 3770*	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 3771	The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul by Eric Schmidt.) (Contributed by NM, 16-Sep-1993.) (Revised by Eric Schmidt, 4-Apr-2007.)
|- U. (/) = (/)
Theorem	elssuni 3772	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 3773	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 3774*	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 3775*	A subclass condition on the members of two classes that implies a subclass relation on their unions. Proposition 8.6 of [TakeutiZaring] p. 59. (Contributed by NM, 22-Mar-2004.)
|- ( A. x e. A E. y e. B x C_ y -> U. A C_ U. B )
Theorem	unidif 3776*	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 3777*	Relationship implying union. (Contributed by NM, 10-Nov-1999.)
|- ( ( A e. B /\ A. x e. B x C_ A ) -> A = U. B )
Theorem	unimax 3778*	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 )
2.1.19  The intersection of a class
Syntax	cint 3779	Extend class notation to include the intersection of a class (read: 'intersect A').
class |^| A
Definition	df-int 3780*	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 3082. (Contributed by NM, 18-Aug-1993.)
|- |^| A = { x | A. y ( y e. A -> x e. y ) }
Theorem	dfint2 3781*	Alternate definition of class intersection. (Contributed by NM, 28-Jun-1998.)
|- |^| A = { x | A. y e. A x e. y }
Theorem	inteq 3782	Equality law for intersection. (Contributed by NM, 13-Sep-1999.)
|- ( A = B -> |^| A = |^| B )
Theorem	inteqi 3783	Equality inference for class intersection. (Contributed by NM, 2-Sep-2003.)
|- A = B   =>    |- |^| A = |^| B
Theorem	inteqd 3784	Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.)
|- ( ph -> A = B )   =>    |- ( ph -> |^| A = |^| B )
Theorem	elint 3785*	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 3786*	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 3787*	Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003.)
|- ( A e. V -> ( A e. |^| B <-> A. x e. B A e. x ) )
Theorem	elinti 3788	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 3789	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 3790*	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 3791*	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 3792*	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 3793	The intersection of the empty set is the universal class. Exercise 2 of [TakeutiZaring] p. 44. (Contributed by NM, 18-Aug-1993.)
|- |^| (/) = _V
Theorem	intss1 3794	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 3795*	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 3796*	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 3797*	Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.)
|- A C_ |^| { x e. B | A C_ x }
Theorem	ssmin 3798*	Subclass of the minimum value of class of supersets. (Contributed by NM, 10-Aug-2006.)
|- A C_ |^| { x | ( A C_ x /\ ph ) }
Theorem	intmin 3799*	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 3800	Intersection of subclasses. (Contributed by NM, 14-Oct-1999.)
|- ( A C_ B -> |^| B C_ |^| A )