P. 34 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3301-3400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ssun2 3301	Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)
|- A C_ ( B u. A )
Theorem	ssun3 3302	Subclass law for union of classes. (Contributed by NM, 5-Aug-1993.)
|- ( A C_ B -> A C_ ( B u. C ) )
Theorem	ssun4 3303	Subclass law for union of classes. (Contributed by NM, 14-Aug-1994.)
|- ( A C_ B -> A C_ ( C u. B ) )
Theorem	elun1 3304	Membership law for union of classes. (Contributed by NM, 5-Aug-1993.)
|- ( A e. B -> A e. ( B u. C ) )
Theorem	elun2 3305	Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)
|- ( A e. B -> A e. ( C u. B ) )
Theorem	unss1 3306	Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A C_ B -> ( A u. C ) C_ ( B u. C ) )
Theorem	ssequn1 3307	A relationship between subclass and union. Theorem 26 of [Suppes] p. 27. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A C_ B <-> ( A u. B ) = B )
Theorem	unss2 3308	Subclass law for union of classes. Exercise 7 of [TakeutiZaring] p. 18. (Contributed by NM, 14-Oct-1999.)
|- ( A C_ B -> ( C u. A ) C_ ( C u. B ) )
Theorem	unss12 3309	Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.)
|- ( ( A C_ B /\ C C_ D ) -> ( A u. C ) C_ ( B u. D ) )
Theorem	ssequn2 3310	A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)
|- ( A C_ B <-> ( B u. A ) = B )
Theorem	unss 3311	The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27 and its converse. (Contributed by NM, 11-Jun-2004.)
|- ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C )
Theorem	unssi 3312	An inference showing the union of two subclasses is a subclass. (Contributed by Raph Levien, 10-Dec-2002.)
|- A C_ C   &    |- B C_ C   =>    |- ( A u. B ) C_ C
Theorem	unssd 3313	A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> A C_ C )   &    |- ( ph -> B C_ C )   =>    |- ( ph -> ( A u. B ) C_ C )
Theorem	unssad 3314	If ( A u. B ) is contained in C, so is A. One-way deduction form of unss 3311. Partial converse of unssd 3313. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> ( A u. B ) C_ C )   =>    |- ( ph -> A C_ C )
Theorem	unssbd 3315	If ( A u. B ) is contained in C, so is B. One-way deduction form of unss 3311. Partial converse of unssd 3313. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> ( A u. B ) C_ C )   =>    |- ( ph -> B C_ C )
Theorem	ssun 3316	A condition that implies inclusion in the union of two classes. (Contributed by NM, 23-Nov-2003.)
|- ( ( A C_ B \/ A C_ C ) -> A C_ ( B u. C ) )
Theorem	rexun 3317	Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011.)
|- ( E. x e. ( A u. B ) ph <-> ( E. x e. A ph \/ E. x e. B ph ) )
Theorem	ralunb 3318	Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ( A. x e. ( A u. B ) ph <-> ( A. x e. A ph /\ A. x e. B ph ) )
Theorem	ralun 3319	Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( A. x e. A ph /\ A. x e. B ph ) -> A. x e. ( A u. B ) ph )
2.1.13.3  The intersection of two classes
Theorem	elin 3320	Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 29-Apr-1994.)
|- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )
Theorem	elini 3321	Membership in an intersection of two classes. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- A e. B   &    |- A e. C   =>    |- A e. ( B i^i C )
Theorem	elind 3322	Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> X e. A )   &    |- ( ph -> X e. B )   =>    |- ( ph -> X e. ( A i^i B ) )
Theorem	elinel1 3323	Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. ( B i^i C ) -> A e. B )
Theorem	elinel2 3324	Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. ( B i^i C ) -> A e. C )
Theorem	elin2 3325	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 3326	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 3327	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 3328	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 3329	Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.)
|- ( A i^i B ) = ( B i^i A )
Theorem	ineqri 3330*	Inference from membership to intersection. (Contributed by NM, 5-Aug-1993.)
|- ( ( x e. A /\ x e. B ) <-> x e. C )   =>    |- ( A i^i B ) = C
Theorem	ineq1 3331	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 3332	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 3333	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 3334	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 3335	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 3336	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 3337	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 3338	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 3339	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 3340	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	dfss1 3341	A frequently-used variant of subclass definition df-ss 3144. (Contributed by NM, 10-Jan-2015.)
|- ( A C_ B <-> ( B i^i A ) = A )
Theorem	dfss5 3342	Another definition of subclasshood. Similar to df-ss 3144, dfss 3145, and dfss1 3341. (Contributed by David Moews, 1-May-2017.)
|- ( A C_ B <-> A = ( B i^i A ) )
Theorem	nfin 3343	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	csbing 3344	Distribute proper substitution through an intersection relation. (Contributed by Alan Sare, 22-Jul-2012.)
|- ( A e. B -> [_ A / x ]_ ( C i^i D ) = ( [_ A / x ]_ C i^i [_ A / x ]_ D ) )
Theorem	rabbi2dva 3345*	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 3346	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 3347	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 3348	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 3349	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 3350	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 3351	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 3352	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 3353	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 3354	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 3355	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	sseqin2 3356	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	inss1 3357	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 3358	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 3359	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 3360	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 3361	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 3362	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 3363	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	ssrind 3364	Add right intersection to subclass relation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A C_ B )   =>    |- ( ph -> ( A i^i C ) C_ ( B i^i C ) )
Theorem	ss2in 3365	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 3366	Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.)
|- ( A C_ C -> ( A i^i B ) C_ C )
Theorem	inss 3367	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  Combinations of difference, union, and intersection of two classes
Theorem	unabs 3368	Absorption law for union. (Contributed by NM, 16-Apr-2006.)
|- ( A u. ( A i^i B ) ) = A
Theorem	inabs 3369	Absorption law for intersection. (Contributed by NM, 16-Apr-2006.)
|- ( A i^i ( A u. B ) ) = A
Theorem	dfss4st 3370*	Subclass defined in terms of class difference. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A. xSTAB x e. A -> ( A C_ B <-> ( B \ ( B \ A ) ) = A ) )
Theorem	ssddif 3371	Double complement and subset. Similar to ddifss 3375 but inside a class B instead of the universal class _V. In classical logic the subset operation on the right hand side could be an equality (that is, A C_ B <-> ( B \ ( B \ A ) ) = A). (Contributed by Jim Kingdon, 24-Jul-2018.)
|- ( A C_ B <-> A C_ ( B \ ( B \ A ) ) )
Theorem	unssdif 3372	Union of two classes and class difference. In classical logic this would be an equality. (Contributed by Jim Kingdon, 24-Jul-2018.)
|- ( A u. B ) C_ ( _V \ ( ( _V \ A ) \ B ) )
Theorem	inssdif 3373	Intersection of two classes and class difference. In classical logic this would be an equality. (Contributed by Jim Kingdon, 24-Jul-2018.)
|- ( A i^i B ) C_ ( A \ ( _V \ B ) )
Theorem	difin 3374	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	ddifss 3375	Double complement under universal class. In classical logic (or given an additional hypothesis, as in ddifnel 3268), this is equality rather than subset. (Contributed by Jim Kingdon, 24-Jul-2018.)
|- A C_ ( _V \ ( _V \ A ) )
Theorem	unssin 3376	Union as a subset of class complement and intersection (De Morgan's law). One direction of the definition of union in [Mendelson] p. 231. This would be an equality, rather than subset, in classical logic. (Contributed by Jim Kingdon, 25-Jul-2018.)
|- ( A u. B ) C_ ( _V \ ( ( _V \ A ) i^i ( _V \ B ) ) )
Theorem	inssun 3377	Intersection in terms of class difference and union (De Morgan's law). Similar to Exercise 4.10(n) of [Mendelson] p. 231. This would be an equality, rather than subset, in classical logic. (Contributed by Jim Kingdon, 25-Jul-2018.)
|- ( A i^i B ) C_ ( _V \ ( ( _V \ A ) u. ( _V \ B ) ) )
Theorem	inssddif 3378	Intersection of two classes and class difference. In classical logic, such as Exercise 4.10(q) of [Mendelson] p. 231, this is an equality rather than subset. (Contributed by Jim Kingdon, 26-Jul-2018.)
|- ( A i^i B ) C_ ( A \ ( A \ B ) )
Theorem	invdif 3379	Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.)
|- ( A i^i ( _V \ B ) ) = ( A \ B )
Theorem	indif 3380	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 3381	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 3382	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 3383	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 3384	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 3385	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 3386	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 3387	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	uneqin 3388	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 3389	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 3390	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
|- ( ( A u. B ) \ C ) = ( ( A \ C ) u. ( B \ C ) )
Theorem	difindiss 3391	Distributive law for class difference. In classical logic, for example, theorem 40 of [Suppes] p. 29, this is an equality instead of subset. (Contributed by Jim Kingdon, 26-Jul-2018.)
|- ( ( A \ B ) u. ( A \ C ) ) C_ ( A \ ( B i^i C ) )
Theorem	difindir 3392	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
|- ( ( A i^i B ) \ C ) = ( ( A \ C ) i^i ( B \ C ) )
Theorem	indifdir 3393	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	difdif2ss 3394	Set difference with a set difference. In classical logic this would be equality rather than subset. (Contributed by Jim Kingdon, 27-Jul-2018.)
|- ( ( A \ B ) u. ( A i^i C ) ) C_ ( A \ ( B \ C ) )
Theorem	undm 3395	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	indmss 3396	De Morgan's law for intersection. In classical logic, this would be equality rather than subset, as in Theorem 5.2(13') of [Stoll] p. 19. (Contributed by Jim Kingdon, 27-Jul-2018.)
|- ( ( _V \ A ) u. ( _V \ B ) ) C_ ( _V \ ( A i^i B ) )
Theorem	difun1 3397	A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004.)
|- ( A \ ( B u. C ) ) = ( ( A \ B ) \ C )
Theorem	undif3ss 3398	A subset relationship involving class union and class difference. In classical logic, this would be equality rather than subset, as in the first equality of Exercise 13 of [TakeutiZaring] p. 22. (Contributed by Jim Kingdon, 28-Jul-2018.)
|- ( A u. ( B \ C ) ) C_ ( ( A u. B ) \ ( C \ A ) )
Theorem	difin2 3399	Represent a set 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 3400	Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004.)
|- ( ( A \ B ) \ C ) = ( ( A \ C ) \ B )