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	ssun 3301	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 3302	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 3303	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 3304	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 3305	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 3306	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 3307	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 3308	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 3309	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 3310	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 3311	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 3312	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 3313	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 3314	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 3315*	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 3316	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 3317	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 3318	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 3319	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 3320	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 3321	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 3322	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 3323	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 3324	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 3325	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 3326	A frequently-used variant of subclass definition df-ss 3129. (Contributed by NM, 10-Jan-2015.)
|- ( A C_ B <-> ( B i^i A ) = A )
Theorem	dfss5 3327	Another definition of subclasshood. Similar to df-ss 3129, dfss 3130, and dfss1 3326. (Contributed by David Moews, 1-May-2017.)
|- ( A C_ B <-> A = ( B i^i A ) )
Theorem	nfin 3328	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 3329	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 3330*	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 3331	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 3332	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 3333	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 3334	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 3335	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 3336	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 3337	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 3338	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 3339	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 3340	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 3341	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 3342	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 3343	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 3344	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 3345	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 3346	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 3347	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 3348	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 3349	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 3350	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 3351	Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.)
|- ( A C_ C -> ( A i^i B ) C_ C )
Theorem	inss 3352	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 3353	Absorption law for union. (Contributed by NM, 16-Apr-2006.)
|- ( A u. ( A i^i B ) ) = A
Theorem	inabs 3354	Absorption law for intersection. (Contributed by NM, 16-Apr-2006.)
|- ( A i^i ( A u. B ) ) = A
Theorem	dfss4st 3355*	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 3356	Double complement and subset. Similar to ddifss 3360 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 3357	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 3358	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 3359	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 3360	Double complement under universal class. In classical logic (or given an additional hypothesis, as in ddifnel 3253), this is equality rather than subset. (Contributed by Jim Kingdon, 24-Jul-2018.)
|- A C_ ( _V \ ( _V \ A ) )
Theorem	unssin 3361	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 3362	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 3363	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 3364	Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.)
|- ( A i^i ( _V \ B ) ) = ( A \ B )
Theorem	indif 3365	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 3366	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 3367	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 3368	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 3369	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 3370	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 3371	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 3372	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 3373	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 3374	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 3375	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
|- ( ( A u. B ) \ C ) = ( ( A \ C ) u. ( B \ C ) )
Theorem	difindiss 3376	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 3377	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
|- ( ( A i^i B ) \ C ) = ( ( A \ C ) i^i ( B \ C ) )
Theorem	indifdir 3378	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 3379	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 3380	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 3381	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 3382	A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004.)
|- ( A \ ( B u. C ) ) = ( ( A \ B ) \ C )
Theorem	undif3ss 3383	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 3384	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 3385	Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004.)
|- ( ( A \ B ) \ C ) = ( ( A \ C ) \ B )
Theorem	difabs 3386	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	symdif1 3387	Two ways to express symmetric difference. This theorem shows the equivalence of the definition of symmetric difference in [Stoll] p. 13 and the restated definition in Example 4.1 of [Stoll] p. 262. (Contributed by NM, 17-Aug-2004.)
|- ( ( A \ B ) u. ( B \ A ) ) = ( ( A u. B ) \ ( A i^i B ) )
2.1.13.5  Class abstractions with difference, union, and intersection of two classes
Theorem	symdifxor 3388*	Expressing symmetric difference with exclusive-or or two differences. (Contributed by Jim Kingdon, 28-Jul-2018.)
|- ( ( A \ B ) u. ( B \ A ) ) = { x | ( x e. A \/_ x e. B ) }
Theorem	unab 3389	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 3390	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 3391	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 3392	A class builder defined by a negation. (Contributed by FL, 18-Sep-2010.)
|- { x | -. ph } = ( _V \ { x | ph } )
Theorem	unrab 3393	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 3394	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 3395*	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 }
Theorem	difrab 3396	Difference of two restricted class abstractions. (Contributed by NM, 23-Oct-2004.)
|- ( { x e. A | ph } \ { x e. A | ps } ) = { x e. A | ( ph /\ -. ps ) }
Theorem	dfrab2 3397*	Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003.)
|- { x e. A | ph } = ( { x | ph } i^i A )
Theorem	dfrab3 3398*	Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
|- { x e. A | ph } = ( A i^i { x | ph } )
Theorem	notrab 3399*	Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( A \ { x e. A | ph } ) = { x e. A | -. ph }
Theorem	dfrab3ss 3400*	Restricted class abstraction with a common superset. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro, 8-Nov-2015.)
|- ( A C_ B -> { x e. A | ph } = ( A i^i { x e. B | ph } ) )