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	sstri 3201	Subclass transitivity inference. (Contributed by NM, 5-May-2000.)
|- A C_ B   &    |- B C_ C   =>    |- A C_ C
Theorem	sstrd 3202	Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)
|- ( ph -> A C_ B )   &    |- ( ph -> B C_ C )   =>    |- ( ph -> A C_ C )
Theorem	sstrid 3203	Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)
|- A C_ B   &    |- ( ph -> B C_ C )   =>    |- ( ph -> A C_ C )
Theorem	sstrdi 3204	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> A C_ B )   &    |- B C_ C   =>    |- ( ph -> A C_ C )
Theorem	sylan9ss 3205	A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ( ph -> A C_ B )   &    |- ( ps -> B C_ C )   =>    |- ( ( ph /\ ps ) -> A C_ C )
Theorem	sylan9ssr 3206	A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.)
|- ( ph -> A C_ B )   &    |- ( ps -> B C_ C )   =>    |- ( ( ps /\ ph ) -> A C_ C )
Theorem	eqss 3207	The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 5-Aug-1993.)
|- ( A = B <-> ( A C_ B /\ B C_ A ) )
Theorem	eqssi 3208	Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.)
|- A C_ B   &    |- B C_ A   =>    |- A = B
Theorem	eqssd 3209	Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.)
|- ( ph -> A C_ B )   &    |- ( ph -> B C_ A )   =>    |- ( ph -> A = B )
Theorem	eqrd 3210	Deduce equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 21-Mar-2017.)
|- F/ x ph   &    |- F/_ x A   &    |- F/_ x B   &    |- ( ph -> ( x e. A <-> x e. B ) )   =>    |- ( ph -> A = B )
Theorem	eqelssd 3211*	Equality deduction from subclass relationship and membership. (Contributed by AV, 21-Aug-2022.)
|- ( ph -> A C_ B )   &    |- ( ( ph /\ x e. B ) -> x e. A )   =>    |- ( ph -> A = B )
Theorem	ssid 3212	Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- A C_ A
Theorem	ssidd 3213	Weakening of ssid 3212. (Contributed by BJ, 1-Sep-2022.)
|- ( ph -> A C_ A )
Theorem	ssv 3214	Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.)
|- A C_ _V
Theorem	sseq1 3215	Equality theorem for subclasses. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
|- ( A = B -> ( A C_ C <-> B C_ C ) )
Theorem	sseq2 3216	Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)
|- ( A = B -> ( C C_ A <-> C C_ B ) )
Theorem	sseq12 3217	Equality theorem for the subclass relationship. (Contributed by NM, 31-May-1999.)
|- ( ( A = B /\ C = D ) -> ( A C_ C <-> B C_ D ) )
Theorem	sseq1i 3218	An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.)
|- A = B   =>    |- ( A C_ C <-> B C_ C )
Theorem	sseq2i 3219	An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.)
|- A = B   =>    |- ( C C_ A <-> C C_ B )
Theorem	sseq12i 3220	An equality inference for the subclass relationship. (Contributed by NM, 31-May-1999.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
|- A = B   &    |- C = D   =>    |- ( A C_ C <-> B C_ D )
Theorem	sseq1d 3221	An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A C_ C <-> B C_ C ) )
Theorem	sseq2d 3222	An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C C_ A <-> C C_ B ) )
Theorem	sseq12d 3223	An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A C_ C <-> B C_ D ) )
Theorem	eqsstri 3224	Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.)
|- A = B   &    |- B C_ C   =>    |- A C_ C
Theorem	eqsstrri 3225	Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.)
|- B = A   &    |- B C_ C   =>    |- A C_ C
Theorem	sseqtri 3226	Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.)
|- A C_ B   &    |- B = C   =>    |- A C_ C
Theorem	sseqtrri 3227	Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)
|- A C_ B   &    |- C = B   =>    |- A C_ C
Theorem	eqsstrd 3228	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
|- ( ph -> A = B )   &    |- ( ph -> B C_ C )   =>    |- ( ph -> A C_ C )
Theorem	eqsstrrd 3229	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
|- ( ph -> B = A )   &    |- ( ph -> B C_ C )   =>    |- ( ph -> A C_ C )
Theorem	sseqtrd 3230	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
|- ( ph -> A C_ B )   &    |- ( ph -> B = C )   =>    |- ( ph -> A C_ C )
Theorem	sseqtrrd 3231	Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
|- ( ph -> A C_ B )   &    |- ( ph -> C = B )   =>    |- ( ph -> A C_ C )
Theorem	3sstr3i 3232	Substitution of equality in both sides of a subclass relationship. (Contributed by NM, 13-Jan-1996.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
|- A C_ B   &    |- A = C   &    |- B = D   =>    |- C C_ D
Theorem	3sstr4i 3233	Substitution of equality in both sides of a subclass relationship. (Contributed by NM, 13-Jan-1996.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
|- A C_ B   &    |- C = A   &    |- D = B   =>    |- C C_ D
Theorem	3sstr3g 3234	Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.)
|- ( ph -> A C_ B )   &    |- A = C   &    |- B = D   =>    |- ( ph -> C C_ D )
Theorem	3sstr4g 3235	Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
|- ( ph -> A C_ B )   &    |- C = A   &    |- D = B   =>    |- ( ph -> C C_ D )
Theorem	3sstr3d 3236	Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.)
|- ( ph -> A C_ B )   &    |- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> C C_ D )
Theorem	3sstr4d 3237	Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 30-Nov-1995.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
|- ( ph -> A C_ B )   &    |- ( ph -> C = A )   &    |- ( ph -> D = B )   =>    |- ( ph -> C C_ D )
Theorem	eqsstrid 3238	B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
|- A = B   &    |- ( ph -> B C_ C )   =>    |- ( ph -> A C_ C )
Theorem	eqsstrrid 3239	B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
|- B = A   &    |- ( ph -> B C_ C )   =>    |- ( ph -> A C_ C )
Theorem	sseqtrdi 3240	A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
|- ( ph -> A C_ B )   &    |- B = C   =>    |- ( ph -> A C_ C )
Theorem	sseqtrrdi 3241	A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
|- ( ph -> A C_ B )   &    |- C = B   =>    |- ( ph -> A C_ C )
Theorem	sseqtrid 3242	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- B C_ A   &    |- ( ph -> A = C )   =>    |- ( ph -> B C_ C )
Theorem	sseqtrrid 3243	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- B C_ A   &    |- ( ph -> C = A )   =>    |- ( ph -> B C_ C )
Theorem	eqsstrdi 3244	A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- ( ph -> A = B )   &    |- B C_ C   =>    |- ( ph -> A C_ C )
Theorem	eqsstrrdi 3245	A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- ( ph -> B = A )   &    |- B C_ C   =>    |- ( ph -> A C_ C )
Theorem	eqimss 3246	Equality implies the subclass relation. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
|- ( A = B -> A C_ B )
Theorem	eqimss2 3247	Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.)
|- ( B = A -> A C_ B )
Theorem	eqimssi 3248	Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.)
|- A = B   =>    |- A C_ B
Theorem	eqimss2i 3249	Infer subclass relationship from equality. (Contributed by NM, 7-Jan-2007.)
|- A = B   =>    |- B C_ A
Theorem	nssne1 3250	Two classes are different if they don't include the same class. (Contributed by NM, 23-Apr-2015.)
|- ( ( A C_ B /\ -. A C_ C ) -> B =/= C )
Theorem	nssne2 3251	Two classes are different if they are not subclasses of the same class. (Contributed by NM, 23-Apr-2015.)
|- ( ( A C_ C /\ -. B C_ C ) -> A =/= B )
Theorem	nssr 3252*	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 3253	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 3254	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 3255	"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 3256*	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 3257*	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 3258*	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 3259*	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 3260	Class abstractions in a subclass relationship. (Contributed by NM, 3-Jul-1994.)
|- ( { x | ph } C_ { x | ps } <-> A. x ( ph -> ps ) )
Theorem	abss 3261*	Class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.)
|- ( { x | ph } C_ A <-> A. x ( ph -> x e. A ) )
Theorem	ssab 3262*	Subclass of a class abstraction. (Contributed by NM, 16-Aug-2006.)
|- ( A C_ { x | ph } <-> A. x ( x e. A -> ph ) )
Theorem	ssabral 3263*	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 3264	Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.)
|- ( ph -> ps )   =>    |- { x | ph } C_ { x | ps }
Theorem	ss2abdv 3265*	Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> { x | ps } C_ { x | ch } )
Theorem	abssdv 3266*	Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
|- ( ph -> ( ps -> x e. A ) )   =>    |- ( ph -> { x | ps } C_ A )
Theorem	abssi 3267*	Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
|- ( ph -> x e. A )   =>    |- { x | ph } C_ A
Theorem	ss2rab 3268	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 3269*	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 3270*	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 3271*	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 3272*	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 3273*	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 3274	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 3275*	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 3276*	Subclass relation for the restriction of a class abstraction. (Contributed by NM, 31-Mar-1995.)
|- { x | ( x e. A /\ ph ) } C_ A
Theorem	ssrab2 3277*	Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.)
|- { x e. A | ph } C_ A
Theorem	ssrab3 3278*	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 3279*	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 3280	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 3281*	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 3282*	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 3283	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 3284	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 3285	Equality theorem for class difference. (Contributed by FL, 31-Aug-2009.)
|- ( ( A = B /\ C = D ) -> ( A \ C ) = ( B \ D ) )
Theorem	difeq1i 3286	Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
|- A = B   =>    |- ( A \ C ) = ( B \ C )
Theorem	difeq2i 3287	Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
|- A = B   =>    |- ( C \ A ) = ( C \ B )
Theorem	difeq12i 3288	Equality inference for class difference. (Contributed by NM, 29-Aug-2004.)
|- A = B   &    |- C = D   =>    |- ( A \ C ) = ( B \ D )
Theorem	difeq1d 3289	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 3290	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 3291	Equality deduction for class difference. (Contributed by FL, 29-May-2014.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A \ C ) = ( B \ D ) )
Theorem	difeqri 3292*	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 3293	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 3294	Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
|- ( A e. ( B \ C ) -> A e. B )
Theorem	eldifn 3295	Implication of membership in a class difference. (Contributed by NM, 3-May-1994.)
|- ( A e. ( B \ C ) -> -. A e. C )
Theorem	elndif 3296	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 3297	Double class difference. Exercise 11 of [TakeutiZaring] p. 22. (Contributed by NM, 17-May-1998.)
|- ( A \ ( B \ A ) ) = A
Theorem	difss 3298	Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
|- ( A \ B ) C_ A
Theorem	difssd 3299	A difference of two classes is contained in the minuend. Deduction form of difss 3298. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> ( A \ B ) C_ A )
Theorem	difss2 3300	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 )