P. 33 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3201-3300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nssr 3201*	Negation of subclass relationship. One direction of Exercise 13 of [TakeutiZaring] p. 18. (Contributed by Jim Kingdon, 15-Jul-2018.)
|- ( E. x ( x e. A /\ -. x e. B ) -> -. A C_ B )
Theorem	nelss 3202	Demonstrate by witnesses that two classes lack a subclass relation. (Contributed by Stefan O'Rear, 5-Feb-2015.)
|- ( ( A e. B /\ -. A e. C ) -> -. B C_ C )
Theorem	ssrexf 3203	Restricted existential quantification follows from a subclass relationship. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A C_ B -> ( E. x e. A ph -> E. x e. B ph ) )
Theorem	ssrmof 3204	"At most one" existential quantification restricted to a subclass. (Contributed by Thierry Arnoux, 8-Oct-2017.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A C_ B -> ( E* x e. B ph -> E* x e. A ph ) )
Theorem	ssralv 3205*	Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.)
|- ( A C_ B -> ( A. x e. B ph -> A. x e. A ph ) )
Theorem	ssrexv 3206*	Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007.)
|- ( A C_ B -> ( E. x e. A ph -> E. x e. B ph ) )
Theorem	ralss 3207*	Restricted universal quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( A C_ B -> ( A. x e. A ph <-> A. x e. B ( x e. A -> ph ) ) )
Theorem	rexss 3208*	Restricted existential quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( A C_ B -> ( E. x e. A ph <-> E. x e. B ( x e. A /\ ph ) ) )
Theorem	ss2ab 3209	Class abstractions in a subclass relationship. (Contributed by NM, 3-Jul-1994.)
|- ( { x | ph } C_ { x | ps } <-> A. x ( ph -> ps ) )
Theorem	abss 3210*	Class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.)
|- ( { x | ph } C_ A <-> A. x ( ph -> x e. A ) )
Theorem	ssab 3211*	Subclass of a class abstraction. (Contributed by NM, 16-Aug-2006.)
|- ( A C_ { x | ph } <-> A. x ( x e. A -> ph ) )
Theorem	ssabral 3212*	The relation for a subclass of a class abstraction is equivalent to restricted quantification. (Contributed by NM, 6-Sep-2006.)
|- ( A C_ { x | ph } <-> A. x e. A ph )
Theorem	ss2abi 3213	Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.)
|- ( ph -> ps )   =>    |- { x | ph } C_ { x | ps }
Theorem	ss2abdv 3214*	Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> { x | ps } C_ { x | ch } )
Theorem	abssdv 3215*	Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
|- ( ph -> ( ps -> x e. A ) )   =>    |- ( ph -> { x | ps } C_ A )
Theorem	abssi 3216*	Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
|- ( ph -> x e. A )   =>    |- { x | ph } C_ A
Theorem	ss2rab 3217	Restricted abstraction classes in a subclass relationship. (Contributed by NM, 30-May-1999.)
|- ( { x e. A | ph } C_ { x e. A | ps } <-> A. x e. A ( ph -> ps ) )
Theorem	rabss 3218*	Restricted class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.)
|- ( { x e. A | ph } C_ B <-> A. x e. A ( ph -> x e. B ) )
Theorem	ssrab 3219*	Subclass of a restricted class abstraction. (Contributed by NM, 16-Aug-2006.)
|- ( B C_ { x e. A | ph } <-> ( B C_ A /\ A. x e. B ph ) )
Theorem	ssrabdv 3220*	Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 31-Aug-2006.)
|- ( ph -> B C_ A )   &    |- ( ( ph /\ x e. B ) -> ps )   =>    |- ( ph -> B C_ { x e. A | ps } )
Theorem	rabssdv 3221*	Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 2-Feb-2015.)
|- ( ( ph /\ x e. A /\ ps ) -> x e. B )   =>    |- ( ph -> { x e. A | ps } C_ B )
Theorem	ss2rabdv 3222*	Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006.)
|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )   =>    |- ( ph -> { x e. A | ps } C_ { x e. A | ch } )
Theorem	ss2rabi 3223	Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999.)
|- ( x e. A -> ( ph -> ps ) )   =>    |- { x e. A | ph } C_ { x e. A | ps }
Theorem	rabss2 3224*	Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A C_ B -> { x e. A | ph } C_ { x e. B | ph } )
Theorem	ssab2 3225*	Subclass relation for the restriction of a class abstraction. (Contributed by NM, 31-Mar-1995.)
|- { x | ( x e. A /\ ph ) } C_ A
Theorem	ssrab2 3226*	Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.)
|- { x e. A | ph } C_ A
Theorem	ssrab3 3227*	Subclass relation for a restricted class abstraction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- B = { x e. A | ph }   =>    |- B C_ A
Theorem	ssrabeq 3228*	If the restricting class of a restricted class abstraction is a subset of this restricted class abstraction, it is equal to this restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.)
|- ( V C_ { x e. V | ph } <-> V = { x e. V | ph } )
Theorem	rabssab 3229	A restricted class is a subclass of the corresponding unrestricted class. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- { x e. A | ph } C_ { x | ph }
Theorem	uniiunlem 3230*	A subset relationship useful for converting union to indexed union using dfiun2 or dfiun2g and intersection to indexed intersection using dfiin2 . (Contributed by NM, 5-Oct-2006.) (Proof shortened by Mario Carneiro, 26-Sep-2015.)
|- ( A. x e. A B e. D -> ( A. x e. A B e. C <-> { y | E. x e. A y = B } C_ C ) )
2.1.13  The difference, union, and intersection of two classes
2.1.13.1  The difference of two classes
Theorem	dfdif3 3231*	Alternate definition of class difference. Definition of relative set complement in Section 2.3 of [Pierik], p. 10. (Contributed by BJ and Jim Kingdon, 16-Jun-2022.)
|- ( A \ B ) = { x e. A | A. y e. B x =/= y }
Theorem	difeq1 3232	Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A = B -> ( A \ C ) = ( B \ C ) )
Theorem	difeq2 3233	Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A = B -> ( C \ A ) = ( C \ B ) )
Theorem	difeq12 3234	Equality theorem for class difference. (Contributed by FL, 31-Aug-2009.)
|- ( ( A = B /\ C = D ) -> ( A \ C ) = ( B \ D ) )
Theorem	difeq1i 3235	Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
|- A = B   =>    |- ( A \ C ) = ( B \ C )
Theorem	difeq2i 3236	Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
|- A = B   =>    |- ( C \ A ) = ( C \ B )
Theorem	difeq12i 3237	Equality inference for class difference. (Contributed by NM, 29-Aug-2004.)
|- A = B   &    |- C = D   =>    |- ( A \ C ) = ( B \ D )
Theorem	difeq1d 3238	Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A \ C ) = ( B \ C ) )
Theorem	difeq2d 3239	Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C \ A ) = ( C \ B ) )
Theorem	difeq12d 3240	Equality deduction for class difference. (Contributed by FL, 29-May-2014.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A \ C ) = ( B \ D ) )
Theorem	difeqri 3241*	Inference from membership to difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( x e. A /\ -. x e. B ) <-> x e. C )   =>    |- ( A \ B ) = C
Theorem	nfdif 3242	Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( A \ B )
Theorem	eldifi 3243	Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
|- ( A e. ( B \ C ) -> A e. B )
Theorem	eldifn 3244	Implication of membership in a class difference. (Contributed by NM, 3-May-1994.)
|- ( A e. ( B \ C ) -> -. A e. C )
Theorem	elndif 3245	A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994.)
|- ( A e. B -> -. A e. ( C \ B ) )
Theorem	difdif 3246	Double class difference. Exercise 11 of [TakeutiZaring] p. 22. (Contributed by NM, 17-May-1998.)
|- ( A \ ( B \ A ) ) = A
Theorem	difss 3247	Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
|- ( A \ B ) C_ A
Theorem	difssd 3248	A difference of two classes is contained in the minuend. Deduction form of difss 3247. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> ( A \ B ) C_ A )
Theorem	difss2 3249	If a class is contained in a difference, it is contained in the minuend. (Contributed by David Moews, 1-May-2017.)
|- ( A C_ ( B \ C ) -> A C_ B )
Theorem	difss2d 3250	If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 3249. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A C_ ( B \ C ) )   =>    |- ( ph -> A C_ B )
Theorem	ssdifss 3251	Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.)
|- ( A C_ B -> ( A \ C ) C_ B )
Theorem	ddifnel 3252*	Double complement under universal class. The hypothesis corresponds to stability of membership in A, which is weaker than decidability (see dcstab 834). Actually, the conclusion is a characterization of stability of membership in a class (see ddifstab 3253) . 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 3359. (Contributed by Jim Kingdon, 21-Jul-2018.)
|- ( -. x e. ( _V \ A ) -> x e. A )   =>    |- ( _V \ ( _V \ A ) ) = A
Theorem	ddifstab 3253*	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 3254	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 3255	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 3256	Difference law for subsets. (Contributed by NM, 28-May-1998.)
|- ( A C_ B -> ( A \ C ) C_ ( B \ C ) )
Theorem	ssdifd 3257	If A is contained in B, then ( A \ C ) is contained in ( B \ C ). Deduction form of ssdif 3256. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A C_ B )   =>    |- ( ph -> ( A \ C ) C_ ( B \ C ) )
Theorem	sscond 3258	If A is contained in B, then ( C \ B ) is contained in ( C \ A ). Deduction form of sscon 3255. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A C_ B )   =>    |- ( ph -> ( C \ B ) C_ ( C \ A ) )
Theorem	ssdifssd 3259	If A is contained in B, then ( A \ C ) is also contained in B. Deduction form of ssdifss 3251. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A C_ B )   =>    |- ( ph -> ( A \ C ) C_ B )
Theorem	ssdif2d 3260	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 3261	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 3262	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 3263*	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 3264	Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
|- ( A u. A ) = A
Theorem	uncom 3265	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 3266	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 3267	Inference form of equncom 3266. (Contributed by Alan Sare, 18-Feb-2012.)
|- A = ( B u. C )   =>    |- A = ( C u. B )
Theorem	uneq1 3268	Equality theorem for union of two classes. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( A u. C ) = ( B u. C ) )
Theorem	uneq2 3269	Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ( C u. A ) = ( C u. B ) )
Theorem	uneq12 3270	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 3271	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 3272	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 3273	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 3274	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 3275	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 3276	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 3277	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 3278	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 3279	A rearrangement of union. (Contributed by NM, 12-Aug-2004.)
|- ( A u. ( B u. C ) ) = ( B u. ( A u. C ) )
Theorem	un23 3280	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 3281	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 3282	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
|- ( A u. ( B u. C ) ) = ( ( A u. B ) u. ( A u. C ) )
Theorem	unundir 3283	Union distributes over itself. (Contributed by NM, 17-Aug-2004.)
|- ( ( A u. B ) u. C ) = ( ( A u. C ) u. ( B u. C ) )
Theorem	ssun1 3284	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 3285	Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)
|- A C_ ( B u. A )
Theorem	ssun3 3286	Subclass law for union of classes. (Contributed by NM, 5-Aug-1993.)
|- ( A C_ B -> A C_ ( B u. C ) )
Theorem	ssun4 3287	Subclass law for union of classes. (Contributed by NM, 14-Aug-1994.)
|- ( A C_ B -> A C_ ( C u. B ) )
Theorem	elun1 3288	Membership law for union of classes. (Contributed by NM, 5-Aug-1993.)
|- ( A e. B -> A e. ( B u. C ) )
Theorem	elun2 3289	Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)
|- ( A e. B -> A e. ( C u. B ) )
Theorem	unss1 3290	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 3291	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 3292	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 3293	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 3294	A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)
|- ( A C_ B <-> ( B u. A ) = B )
Theorem	unss 3295	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 3296	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 3297	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 3298	If ( A u. B ) is contained in C, so is A. One-way deduction form of unss 3295. Partial converse of unssd 3297. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> ( A u. B ) C_ C )   =>    |- ( ph -> A C_ C )
Theorem	unssbd 3299	If ( A u. B ) is contained in C, so is B. One-way deduction form of unss 3295. Partial converse of unssd 3297. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> ( A u. B ) C_ C )   =>    |- ( ph -> B C_ C )
Theorem	ssun 3300	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 ) )