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	difss2d 3301	If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 3300. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A C_ ( B \ C ) )   =>    |- ( ph -> A C_ B )
Theorem	ssdifss 3302	Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.)
|- ( A C_ B -> ( A \ C ) C_ B )
Theorem	ddifnel 3303*	Double complement under universal class. The hypothesis corresponds to stability of membership in A, which is weaker than decidability (see dcstab 845). Actually, the conclusion is a characterization of stability of membership in a class (see ddifstab 3304) . Exercise 4.10(s) of [Mendelson] p. 231, but with an additional hypothesis. For a version without a hypothesis, but which only states that A is a subset of _V \ ( _V \ A ), see ddifss 3410. (Contributed by Jim Kingdon, 21-Jul-2018.)
|- ( -. x e. ( _V \ A ) -> x e. A )   =>    |- ( _V \ ( _V \ A ) ) = A
Theorem	ddifstab 3304*	A class is equal to its double complement if and only if it is stable (that is, membership in it is a stable property). (Contributed by BJ, 12-Dec-2021.)
|- ( ( _V \ ( _V \ A ) ) = A <-> A. xSTAB x e. A )
Theorem	ssconb 3305	Contraposition law for subsets. (Contributed by NM, 22-Mar-1998.)
|- ( ( A C_ C /\ B C_ C ) -> ( A C_ ( C \ B ) <-> B C_ ( C \ A ) ) )
Theorem	sscon 3306	Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.)
|- ( A C_ B -> ( C \ B ) C_ ( C \ A ) )
Theorem	ssdif 3307	Difference law for subsets. (Contributed by NM, 28-May-1998.)
|- ( A C_ B -> ( A \ C ) C_ ( B \ C ) )
Theorem	ssdifd 3308	If A is contained in B, then ( A \ C ) is contained in ( B \ C ). Deduction form of ssdif 3307. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A C_ B )   =>    |- ( ph -> ( A \ C ) C_ ( B \ C ) )
Theorem	sscond 3309	If A is contained in B, then ( C \ B ) is contained in ( C \ A ). Deduction form of sscon 3306. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A C_ B )   =>    |- ( ph -> ( C \ B ) C_ ( C \ A ) )
Theorem	ssdifssd 3310	If A is contained in B, then ( A \ C ) is also contained in B. Deduction form of ssdifss 3302. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A C_ B )   =>    |- ( ph -> ( A \ C ) C_ B )
Theorem	ssdif2d 3311	If A is contained in B and C is contained in D, then ( A \ D ) is contained in ( B \ C ). Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A C_ B )   &    |- ( ph -> C C_ D )   =>    |- ( ph -> ( A \ D ) C_ ( B \ C ) )
Theorem	raldifb 3312	Restricted universal quantification on a class difference in terms of an implication. (Contributed by Alexander van der Vekens, 3-Jan-2018.)
|- ( A. x e. A ( x e/ B -> ph ) <-> A. x e. ( A \ B ) ph )
2.1.13.2  The union of two classes
Theorem	elun 3313	Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.)
|- ( A e. ( B u. C ) <-> ( A e. B \/ A e. C ) )
Theorem	uneqri 3314*	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 3315	Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
|- ( A u. A ) = A
Theorem	uncom 3316	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 3317	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 3318	Inference form of equncom 3317. (Contributed by Alan Sare, 18-Feb-2012.)
|- A = ( B u. C )   =>    |- A = ( C u. B )
Theorem	uneq1 3319	Equality theorem for union of two classes. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( A u. C ) = ( B u. C ) )
Theorem	uneq2 3320	Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( C u. A ) = ( C u. B ) )
Theorem	uneq12 3321	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 3322	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 3323	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 3324	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 3325	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 3326	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 3327	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 3328	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 3329	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 3330	A rearrangement of union. (Contributed by NM, 12-Aug-2004.)
|- ( A u. ( B u. C ) ) = ( B u. ( A u. C ) )
Theorem	un23 3331	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 3332	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 3333	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
|- ( A u. ( B u. C ) ) = ( ( A u. B ) u. ( A u. C ) )
Theorem	unundir 3334	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
|- ( ( A u. B ) u. C ) = ( ( A u. C ) u. ( B u. C ) )
Theorem	ssun1 3335	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 3336	Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)
|- A C_ ( B u. A )
Theorem	ssun3 3337	Subclass law for union of classes. (Contributed by NM, 5-Aug-1993.)
|- ( A C_ B -> A C_ ( B u. C ) )
Theorem	ssun4 3338	Subclass law for union of classes. (Contributed by NM, 14-Aug-1994.)
|- ( A C_ B -> A C_ ( C u. B ) )
Theorem	elun1 3339	Membership law for union of classes. (Contributed by NM, 5-Aug-1993.)
|- ( A e. B -> A e. ( B u. C ) )
Theorem	elun2 3340	Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)
|- ( A e. B -> A e. ( C u. B ) )
Theorem	unss1 3341	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 3342	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 3343	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 3344	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 3345	A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)
|- ( A C_ B <-> ( B u. A ) = B )
Theorem	unss 3346	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 3347	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 3348	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 3349	If ( A u. B ) is contained in C, so is A. One-way deduction form of unss 3346. Partial converse of unssd 3348. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> ( A u. B ) C_ C )   =>    |- ( ph -> A C_ C )
Theorem	unssbd 3350	If ( A u. B ) is contained in C, so is B. One-way deduction form of unss 3346. Partial converse of unssd 3348. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> ( A u. B ) C_ C )   =>    |- ( ph -> B C_ C )
Theorem	ssun 3351	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 3352	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 3353	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 3354	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 3355	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 3356	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 3357	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 3358	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 3359	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 3360	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 3361	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 3362	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 3363	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 3364	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 3365*	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 3366	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 3367	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 3368	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 3369	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 3370	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 3371	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 3372	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 3373	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 3374	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 3375	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 3376	A frequently-used variant of subclass definition df-ss 3178. (Contributed by NM, 10-Jan-2015.)
|- ( A C_ B <-> ( B i^i A ) = A )
Theorem	dfss5 3377	Another definition of subclasshood. Similar to df-ss 3178, dfss 3179, and dfss1 3376. (Contributed by David Moews, 1-May-2017.)
|- ( A C_ B <-> A = ( B i^i A ) )
Theorem	nfin 3378	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 3379	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 3380*	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 3381	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 3382	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 3383	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 3384	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 3385	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 3386	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 3387	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 3388	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 3389	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 3390	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 3391	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 3392	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 3393	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 3394	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 3395	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 3396	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 3397	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 3398	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 3399	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 3400	Intersection of subclasses. (Contributed by NM, 5-May-2000.)
|- ( ( A C_ B /\ C C_ D ) -> ( A i^i C ) C_ ( B i^i D ) )