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	uneqri 3301*	Inference from membership to union. (Contributed by NM, 5-Aug-1993.)
|- ( ( x e. A \/ x e. B ) <-> x e. C )   =>    |- ( A u. B ) = C
Theorem	unidm 3302	Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
|- ( A u. A ) = A
Theorem	uncom 3303	Commutative law for union of classes. Exercise 6 of [TakeutiZaring] p. 17. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A u. B ) = ( B u. A )
Theorem	equncom 3304	If a class equals the union of two other classes, then it equals the union of those two classes commuted. (Contributed by Alan Sare, 18-Feb-2012.)
|- ( A = ( B u. C ) <-> A = ( C u. B ) )
Theorem	equncomi 3305	Inference form of equncom 3304. (Contributed by Alan Sare, 18-Feb-2012.)
|- A = ( B u. C )   =>    |- A = ( C u. B )
Theorem	uneq1 3306	Equality theorem for union of two classes. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( A u. C ) = ( B u. C ) )
Theorem	uneq2 3307	Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( C u. A ) = ( C u. B ) )
Theorem	uneq12 3308	Equality theorem for union of two classes. (Contributed by NM, 29-Mar-1998.)
|- ( ( A = B /\ C = D ) -> ( A u. C ) = ( B u. D ) )
Theorem	uneq1i 3309	Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.)
|- A = B   =>    |- ( A u. C ) = ( B u. C )
Theorem	uneq2i 3310	Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.)
|- A = B   =>    |- ( C u. A ) = ( C u. B )
Theorem	uneq12i 3311	Equality inference for union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
|- A = B   &    |- C = D   =>    |- ( A u. C ) = ( B u. D )
Theorem	uneq1d 3312	Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A u. C ) = ( B u. C ) )
Theorem	uneq2d 3313	Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C u. A ) = ( C u. B ) )
Theorem	uneq12d 3314	Equality deduction for union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A u. C ) = ( B u. D ) )
Theorem	nfun 3315	Bound-variable hypothesis builder for the union of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( A u. B )
Theorem	unass 3316	Associative law for union of classes. Exercise 8 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( A u. B ) u. C ) = ( A u. ( B u. C ) )
Theorem	un12 3317	A rearrangement of union. (Contributed by NM, 12-Aug-2004.)
|- ( A u. ( B u. C ) ) = ( B u. ( A u. C ) )
Theorem	un23 3318	A rearrangement of union. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( A u. B ) u. C ) = ( ( A u. C ) u. B )
Theorem	un4 3319	A rearrangement of the union of 4 classes. (Contributed by NM, 12-Aug-2004.)
|- ( ( A u. B ) u. ( C u. D ) ) = ( ( A u. C ) u. ( B u. D ) )
Theorem	unundi 3320	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
|- ( A u. ( B u. C ) ) = ( ( A u. B ) u. ( A u. C ) )
Theorem	unundir 3321	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
|- ( ( A u. B ) u. C ) = ( ( A u. C ) u. ( B u. C ) )
Theorem	ssun1 3322	Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
|- A C_ ( A u. B )
Theorem	ssun2 3323	Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)
|- A C_ ( B u. A )
Theorem	ssun3 3324	Subclass law for union of classes. (Contributed by NM, 5-Aug-1993.)
|- ( A C_ B -> A C_ ( B u. C ) )
Theorem	ssun4 3325	Subclass law for union of classes. (Contributed by NM, 14-Aug-1994.)
|- ( A C_ B -> A C_ ( C u. B ) )
Theorem	elun1 3326	Membership law for union of classes. (Contributed by NM, 5-Aug-1993.)
|- ( A e. B -> A e. ( B u. C ) )
Theorem	elun2 3327	Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)
|- ( A e. B -> A e. ( C u. B ) )
Theorem	unss1 3328	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 3329	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 3330	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 3331	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 3332	A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)
|- ( A C_ B <-> ( B u. A ) = B )
Theorem	unss 3333	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 3334	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 3335	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 3336	If ( A u. B ) is contained in C, so is A. One-way deduction form of unss 3333. Partial converse of unssd 3335. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> ( A u. B ) C_ C )   =>    |- ( ph -> A C_ C )
Theorem	unssbd 3337	If ( A u. B ) is contained in C, so is B. One-way deduction form of unss 3333. Partial converse of unssd 3335. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> ( A u. B ) C_ C )   =>    |- ( ph -> B C_ C )
Theorem	ssun 3338	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 3339	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 3340	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 3341	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 3342	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 3343	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 3344	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 3345	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 3346	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 3347	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 3348	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 3349	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 3350	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 3351	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 3352*	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 3353	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 3354	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 3355	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 3356	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 3357	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 3358	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 3359	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 3360	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 3361	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 3362	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 3363	A frequently-used variant of subclass definition df-ss 3166. (Contributed by NM, 10-Jan-2015.)
|- ( A C_ B <-> ( B i^i A ) = A )
Theorem	dfss5 3364	Another definition of subclasshood. Similar to df-ss 3166, dfss 3167, and dfss1 3363. (Contributed by David Moews, 1-May-2017.)
|- ( A C_ B <-> A = ( B i^i A ) )
Theorem	nfin 3365	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 3366	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 3367*	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 3368	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 3369	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 3370	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 3371	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 3372	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 3373	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 3374	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 3375	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 3376	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 3377	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 3378	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 3379	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 3380	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 3381	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 3382	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 3383	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 3384	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 3385	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 3386	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 3387	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 3388	Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.)
|- ( A C_ C -> ( A i^i B ) C_ C )
Theorem	inss 3389	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 3390	Absorption law for union. (Contributed by NM, 16-Apr-2006.)
|- ( A u. ( A i^i B ) ) = A
Theorem	inabs 3391	Absorption law for intersection. (Contributed by NM, 16-Apr-2006.)
|- ( A i^i ( A u. B ) ) = A
Theorem	dfss4st 3392*	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 3393	Double complement and subset. Similar to ddifss 3397 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 3394	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 3395	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 3396	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 3397	Double complement under universal class. In classical logic (or given an additional hypothesis, as in ddifnel 3290), this is equality rather than subset. (Contributed by Jim Kingdon, 24-Jul-2018.)
|- A C_ ( _V \ ( _V \ A ) )
Theorem	unssin 3398	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 3399	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 3400	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 ) )