P. 39 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 3801-3900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elin2 3801	Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- X = ( B i^i C )   =>    |- ( A e. X <-> ( A e. B /\ A e. C ) )
Theorem	elin1d 3802	Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.)
|- ( ph -> X e. ( A i^i B ) )   =>    |- ( ph -> X e. A )
Theorem	elin2d 3803	Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.)
|- ( ph -> X e. ( A i^i B ) )   =>    |- ( ph -> X e. B )
Theorem	elin3 3804	Membership in a class defined as a ternary intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- X = ( ( B i^i C ) i^i D )   =>    |- ( A e. X <-> ( A e. B /\ A e. C /\ A e. D ) )
Theorem	incom 3805	Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-1993.)
|- ( A i^i B ) = ( B i^i A )
Theorem	ineqri 3806*	Inference from membership to intersection. (Contributed by NM, 21-Jun-1993.)
|- ( ( x e. A /\ x e. B ) <-> x e. C )   =>    |- ( A i^i B ) = C
Theorem	ineq1 3807	Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.)
|- ( A = B -> ( A i^i C ) = ( B i^i C ) )
Theorem	ineq2 3808	Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
|- ( A = B -> ( C i^i A ) = ( C i^i B ) )
Theorem	ineq12 3809	Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.)
|- ( ( A = B /\ C = D ) -> ( A i^i C ) = ( B i^i D ) )
Theorem	ineq1i 3810	Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
|- A = B   =>    |- ( A i^i C ) = ( B i^i C )
Theorem	ineq2i 3811	Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
|- A = B   =>    |- ( C i^i A ) = ( C i^i B )
Theorem	ineq12i 3812	Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
|- A = B   &    |- C = D   =>    |- ( A i^i C ) = ( B i^i D )
Theorem	ineq1d 3813	Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A i^i C ) = ( B i^i C ) )
Theorem	ineq2d 3814	Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C i^i A ) = ( C i^i B ) )
Theorem	ineq12d 3815	Equality deduction for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A i^i C ) = ( B i^i D ) )
Theorem	ineqan12d 3816	Equality deduction for intersection of two classes. (Contributed by NM, 7-Feb-2007.)
|- ( ph -> A = B )   &    |- ( ps -> C = D )   =>    |- ( ( ph /\ ps ) -> ( A i^i C ) = ( B i^i D ) )
Theorem	sseqin2 3817	A relationship between subclass and intersection. Similar to Exercise 9 of [TakeutiZaring] p. 18. (Contributed by NM, 17-May-1994.)
|- ( A C_ B <-> ( B i^i A ) = A )
Theorem	dfss1OLD 3818	Obsolete as of 22-Jul-2021. (Contributed by NM, 10-Jan-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A C_ B <-> ( B i^i A ) = A )
Theorem	dfss5OLD 3819	Obsolete as of 22-Jul-2021. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A C_ B <-> A = ( B i^i A ) )
Theorem	nfin 3820	Bound-variable hypothesis builder for the intersection of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( A i^i B )
Theorem	rabbi2dva 3821*	Deduction from a wff to a restricted class abstraction. (Contributed by NM, 14-Jan-2014.)
|- ( ( ph /\ x e. A ) -> ( x e. B <-> ps ) )   =>    |- ( ph -> ( A i^i B ) = { x e. A | ps } )
Theorem	inidm 3822	Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.)
|- ( A i^i A ) = A
Theorem	inass 3823	Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.)
|- ( ( A i^i B ) i^i C ) = ( A i^i ( B i^i C ) )
Theorem	in12 3824	A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.)
|- ( A i^i ( B i^i C ) ) = ( B i^i ( A i^i C ) )
Theorem	in32 3825	A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( A i^i B ) i^i C ) = ( ( A i^i C ) i^i B )
Theorem	in13 3826	A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
|- ( A i^i ( B i^i C ) ) = ( C i^i ( B i^i A ) )
Theorem	in31 3827	A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
|- ( ( A i^i B ) i^i C ) = ( ( C i^i B ) i^i A )
Theorem	inrot 3828	Rotate the intersection of 3 classes. (Contributed by NM, 27-Aug-2012.)
|- ( ( A i^i B ) i^i C ) = ( ( C i^i A ) i^i B )
Theorem	in4 3829	Rearrangement of intersection of 4 classes. (Contributed by NM, 21-Apr-2001.)
|- ( ( A i^i B ) i^i ( C i^i D ) ) = ( ( A i^i C ) i^i ( B i^i D ) )
Theorem	inindi 3830	Intersection distributes over itself. (Contributed by NM, 6-May-1994.)
|- ( A i^i ( B i^i C ) ) = ( ( A i^i B ) i^i ( A i^i C ) )
Theorem	inindir 3831	Intersection distributes over itself. (Contributed by NM, 17-Aug-2004.)
|- ( ( A i^i B ) i^i C ) = ( ( A i^i C ) i^i ( B i^i C ) )
Theorem	sseqin2OLD 3832	Obsolete proof of sseqin2 3817 as of 22-Jul-2021. (Contributed by NM, 17-May-1994.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A C_ B <-> ( B i^i A ) = A )
Theorem	inss1 3833	The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.)
|- ( A i^i B ) C_ A
Theorem	inss2 3834	The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.)
|- ( A i^i B ) C_ B
Theorem	ssin 3835	Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26. (Contributed by NM, 15-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( A C_ B /\ A C_ C ) <-> A C_ ( B i^i C ) )
Theorem	ssini 3836	An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24-Nov-2003.)
|- A C_ B   &    |- A C_ C   =>    |- A C_ ( B i^i C )
Theorem	ssind 3837	A deduction showing that a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> A C_ B )   &    |- ( ph -> A C_ C )   =>    |- ( ph -> A C_ ( B i^i C ) )
Theorem	ssrin 3838	Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A C_ B -> ( A i^i C ) C_ ( B i^i C ) )
Theorem	sslin 3839	Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.)
|- ( A C_ B -> ( C i^i A ) C_ ( C i^i B ) )
Theorem	ss2in 3840	Intersection of subclasses. (Contributed by NM, 5-May-2000.)
|- ( ( A C_ B /\ C C_ D ) -> ( A i^i C ) C_ ( B i^i D ) )
Theorem	ssinss1 3841	Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.)
|- ( A C_ C -> ( A i^i B ) C_ C )
Theorem	inss 3842	Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014.)
|- ( ( A C_ C \/ B C_ C ) -> ( A i^i B ) C_ C )
2.1.13.4  The symmetric difference of two classes
Syntax	csymdif 3843	Declare the syntax for symmetric difference.
class ( A /_\ B )
Definition	df-symdif 3844	Define the symmetric difference of two classes. (Contributed by Scott Fenton, 31-Mar-2012.)
|- ( A /_\ B ) = ( ( A \ B ) u. ( B \ A ) )
Theorem	symdifcom 3845	Symmetric difference commutes. (Contributed by Scott Fenton, 24-Apr-2012.)
|- ( A /_\ B ) = ( B /_\ A )
Theorem	symdifeq1 3846	Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.)
|- ( A = B -> ( A /_\ C ) = ( B /_\ C ) )
Theorem	symdifeq2 3847	Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.)
|- ( A = B -> ( C /_\ A ) = ( C /_\ B ) )
Theorem	nfsymdif 3848	Hypothesis builder for symmetric difference. (Contributed by Scott Fenton, 19-Feb-2013.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( A /_\ B )
Theorem	elsymdif 3849	Membership in a symmetric difference. (Contributed by Scott Fenton, 31-Mar-2012.)
|- ( A e. ( B /_\ C ) <-> -. ( A e. B <-> A e. C ) )
Theorem	elsymdifxor 3850	Membership in a symmetric difference is an exclusive-or relationship. (Contributed by David A. Wheeler, 26-Apr-2020.)
|- ( A e. ( B /_\ C ) <-> ( A e. B \/_ A e. C ) )
Theorem	dfsymdif2 3851*	Alternate definition of the symmetric difference. (Contributed by BJ, 30-Apr-2020.)
|- ( A /_\ B ) = { x | ( x e. A \/_ x e. B ) }
Theorem	symdif2 3852*	Two ways to express symmetric difference. (Contributed by NM, 17-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( A \ B ) u. ( B \ A ) ) = { x | -. ( x e. A <-> x e. B ) }
Theorem	symdifass 3853	Symmetric difference associates. (Contributed by Scott Fenton, 24-Apr-2012.)
|- ( A /_\ ( B /_\ C ) ) = ( ( A /_\ B ) /_\ C )
2.1.13.5  Combinations of difference, union, and intersection of two classes
Theorem	unabs 3854	Absorption law for union. (Contributed by NM, 16-Apr-2006.)
|- ( A u. ( A i^i B ) ) = A
Theorem	inabs 3855	Absorption law for intersection. (Contributed by NM, 16-Apr-2006.)
|- ( A i^i ( A u. B ) ) = A
Theorem	nssinpss 3856	Negation of subclass expressed in terms of intersection and proper subclass. (Contributed by NM, 30-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( -. A C_ B <-> ( A i^i B ) C. A )
Theorem	nsspssun 3857	Negation of subclass expressed in terms of proper subclass and union. (Contributed by NM, 15-Sep-2004.)
|- ( -. A C_ B <-> B C. ( A u. B ) )
Theorem	dfss4 3858	Subclass defined in terms of class difference. See comments under dfun2 3859. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A C_ B <-> ( B \ ( B \ A ) ) = A )
Theorem	dfun2 3859	An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 3860 and dfss4 3858 it shows we can express union, intersection, and subset directly in terms of the single "primitive" operation \ (class difference). (Contributed by NM, 10-Jun-2004.)
|- ( A u. B ) = ( _V \ ( ( _V \ A ) \ B ) )
Theorem	dfin2 3860	An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 3859. Another version is given by dfin4 3867. (Contributed by NM, 10-Jun-2004.)
|- ( A i^i B ) = ( A \ ( _V \ B ) )
Theorem	difin 3861	Difference with intersection. Theorem 33 of [Suppes] p. 29. (Contributed by NM, 31-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A \ ( A i^i B ) ) = ( A \ B )
Theorem	ssdifim 3862	Implication of a class difference with a subclass. (Contributed by AV, 3-Jan-2022.)
|- ( ( A C_ V /\ B = ( V \ A ) ) -> A = ( V \ B ) )
Theorem	ssdifsym 3863	Symmetric class differences for subclasses. (Contributed by AV, 3-Jan-2022.)
|- ( ( A C_ V /\ B C_ V ) -> ( B = ( V \ A ) <-> A = ( V \ B ) ) )
Theorem	dfss5 3864*	Alternate definition of subclass relationship: a class A is a subclass of another class B iff each element of A is equal to an element of B. (Contributed by AV, 13-Nov-2020.)
|- ( A C_ B <-> A. x e. A E. y e. B x = y )
Theorem	dfun3 3865	Union defined in terms of intersection (De Morgan's law). Definition of union in [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.)
|- ( A u. B ) = ( _V \ ( ( _V \ A ) i^i ( _V \ B ) ) )
Theorem	dfin3 3866	Intersection defined in terms of union (De Morgan's law). Similar to Exercise 4.10(n) of [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.)
|- ( A i^i B ) = ( _V \ ( ( _V \ A ) u. ( _V \ B ) ) )
Theorem	dfin4 3867	Alternate definition of the intersection of two classes. Exercise 4.10(q) of [Mendelson] p. 231. (Contributed by NM, 25-Nov-2003.)
|- ( A i^i B ) = ( A \ ( A \ B ) )
Theorem	invdif 3868	Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.)
|- ( A i^i ( _V \ B ) ) = ( A \ B )
Theorem	indif 3869	Intersection with class difference. Theorem 34 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
|- ( A i^i ( A \ B ) ) = ( A \ B )
Theorem	indif2 3870	Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.)
|- ( A i^i ( B \ C ) ) = ( ( A i^i B ) \ C )
Theorem	indif1 3871	Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015.)
|- ( ( A \ C ) i^i B ) = ( ( A i^i B ) \ C )
Theorem	indifcom 3872	Commutation law for intersection and difference. (Contributed by Scott Fenton, 18-Feb-2013.)
|- ( A i^i ( B \ C ) ) = ( B i^i ( A \ C ) )
Theorem	indi 3873	Distributive law for intersection over union. Exercise 10 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A i^i ( B u. C ) ) = ( ( A i^i B ) u. ( A i^i C ) )
Theorem	undi 3874	Distributive law for union over intersection. Exercise 11 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A u. ( B i^i C ) ) = ( ( A u. B ) i^i ( A u. C ) )
Theorem	indir 3875	Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
|- ( ( A u. B ) i^i C ) = ( ( A i^i C ) u. ( B i^i C ) )
Theorem	undir 3876	Distributive law for union over intersection. Theorem 29 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
|- ( ( A i^i B ) u. C ) = ( ( A u. C ) i^i ( B u. C ) )
Theorem	unineq 3877	Infer equality from equalities of union and intersection. Exercise 20 of [Enderton] p. 32 and its converse. (Contributed by NM, 10-Aug-2004.)
|- ( ( ( A u. C ) = ( B u. C ) /\ ( A i^i C ) = ( B i^i C ) ) <-> A = B )
Theorem	uneqin 3878	Equality of union and intersection implies equality of their arguments. (Contributed by NM, 16-Apr-2006.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( A u. B ) = ( A i^i B ) <-> A = B )
Theorem	difundi 3879	Distributive law for class difference. Theorem 39 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
|- ( A \ ( B u. C ) ) = ( ( A \ B ) i^i ( A \ C ) )
Theorem	difundir 3880	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
|- ( ( A u. B ) \ C ) = ( ( A \ C ) u. ( B \ C ) )
Theorem	difindi 3881	Distributive law for class difference. Theorem 40 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
|- ( A \ ( B i^i C ) ) = ( ( A \ B ) u. ( A \ C ) )
Theorem	difindir 3882	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
|- ( ( A i^i B ) \ C ) = ( ( A \ C ) i^i ( B \ C ) )
Theorem	indifdir 3883	Distribute intersection over difference. (Contributed by Scott Fenton, 14-Apr-2011.)
|- ( ( A \ B ) i^i C ) = ( ( A i^i C ) \ ( B i^i C ) )
Theorem	difdif2 3884	Class difference by a class difference. (Contributed by Thierry Arnoux, 18-Dec-2017.)
|- ( A \ ( B \ C ) ) = ( ( A \ B ) u. ( A i^i C ) )
Theorem	undm 3885	De Morgan's law for union. Theorem 5.2(13) of [Stoll] p. 19. (Contributed by NM, 18-Aug-2004.)
|- ( _V \ ( A u. B ) ) = ( ( _V \ A ) i^i ( _V \ B ) )
Theorem	indm 3886	De Morgan's law for intersection. Theorem 5.2(13') of [Stoll] p. 19. (Contributed by NM, 18-Aug-2004.)
|- ( _V \ ( A i^i B ) ) = ( ( _V \ A ) u. ( _V \ B ) )
Theorem	difun1 3887	A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004.)
|- ( A \ ( B u. C ) ) = ( ( A \ B ) \ C )
Theorem	undif3 3888	An equality involving class union and class difference. The first equality of Exercise 13 of [TakeutiZaring] p. 22. (Contributed by Alan Sare, 17-Apr-2012.) (Proof shortened by JJ, 13-Jul-2021.)
|- ( A u. ( B \ C ) ) = ( ( A u. B ) \ ( C \ A ) )
Theorem	undif3OLD 3889	Obsolete proof of undif3 3888 as of 13-Jul-2021. (Contributed by Alan Sare, 17-Apr-2012.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A u. ( B \ C ) ) = ( ( A u. B ) \ ( C \ A ) )
Theorem	difin2 3890	Represent a class difference as an intersection with a larger difference. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( A C_ C -> ( A \ B ) = ( ( C \ B ) i^i A ) )
Theorem	dif32 3891	Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004.)
|- ( ( A \ B ) \ C ) = ( ( A \ C ) \ B )
Theorem	difabs 3892	Absorption-like law for class difference: you can remove a class only once. (Contributed by FL, 2-Aug-2009.)
|- ( ( A \ B ) \ B ) = ( A \ B )
Theorem	dfsymdif3 3893	Alternate definition of the symmetric difference, given in Example 4.1 of [Stoll] p. 262 (the original definition corresponds to [Stoll] p. 13). (Contributed by NM, 17-Aug-2004.) (Revised by BJ, 30-Apr-2020.)
|- ( A /_\ B ) = ( ( A u. B ) \ ( A i^i B ) )
2.1.13.6  Class abstractions with difference, union, and intersection of two classes
Theorem	unab 3894	Union of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( { x | ph } u. { x | ps } ) = { x | ( ph \/ ps ) }
Theorem	inab 3895	Intersection of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( { x | ph } i^i { x | ps } ) = { x | ( ph /\ ps ) }
Theorem	difab 3896	Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( { x | ph } \ { x | ps } ) = { x | ( ph /\ -. ps ) }
Theorem	notab 3897	A class builder defined by a negation. (Contributed by FL, 18-Sep-2010.)
|- { x | -. ph } = ( _V \ { x | ph } )
Theorem	unrab 3898	Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004.)
|- ( { x e. A | ph } u. { x e. A | ps } ) = { x e. A | ( ph \/ ps ) }
Theorem	inrab 3899	Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.)
|- ( { x e. A | ph } i^i { x e. A | ps } ) = { x e. A | ( ph /\ ps ) }
Theorem	inrab2 3900*	Intersection with a restricted class abstraction. (Contributed by NM, 19-Nov-2007.)
|- ( { x e. A | ph } i^i B ) = { x e. ( A i^i B ) | ph }