P. 31 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3001-3100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	difjust 3001*	Soundness justification theorem for df-dif 3002. (Contributed by Rodolfo Medina, 27-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- { x | ( x e. A /\ -. x e. B ) } = { y | ( y e. A /\ -. y e. B ) }
Definition	df-dif 3002*	Define class difference, also called relative complement. Definition 5.12 of [TakeutiZaring] p. 20. Contrast this operation with union ( A u. B ) (df-un 3004) and intersection ( A i^i B ) (df-in 3006). Several notations are used in the literature; we chose the \ convention used in Definition 5.3 of [Eisenberg] p. 67 instead of the more common minus sign to reserve the latter for later use in, e.g., arithmetic. We will use the terminology " A excludes B " to mean A \ B. We will use " B is removed from A " to mean A \ { B } i.e. the removal of an element or equivalently the exclusion of a singleton. (Contributed by NM, 29-Apr-1994.)
|- ( A \ B ) = { x | ( x e. A /\ -. x e. B ) }
Theorem	unjust 3003*	Soundness justification theorem for df-un 3004. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- { x | ( x e. A \/ x e. B ) } = { y | ( y e. A \/ y e. B ) }
Definition	df-un 3004*	Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. Contrast this operation with difference ( A \ B ) (df-dif 3002) and intersection ( A i^i B ) (df-in 3006). (Contributed by NM, 23-Aug-1993.)
|- ( A u. B ) = { x | ( x e. A \/ x e. B ) }
Theorem	injust 3005*	Soundness justification theorem for df-in 3006. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- { x | ( x e. A /\ x e. B ) } = { y | ( y e. A /\ y e. B ) }
Definition	df-in 3006*	Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. Contrast this operation with union ( A u. B ) (df-un 3004) and difference ( A \ B ) (df-dif 3002). (Contributed by NM, 29-Apr-1994.)
|- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
Theorem	dfin5 3007*	Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005.)
|- ( A i^i B ) = { x e. A | x e. B }
Theorem	dfdif2 3008*	Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.)
|- ( A \ B ) = { x e. A | -. x e. B }
Theorem	eldif 3009	Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
|- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )
Theorem	eldifd 3010	If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3009. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. B )   &    |- ( ph -> -. A e. C )   =>    |- ( ph -> A e. ( B \ C ) )
Theorem	eldifad 3011	If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3009. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. ( B \ C ) )   =>    |- ( ph -> A e. B )
Theorem	eldifbd 3012	If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3009. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. ( B \ C ) )   =>    |- ( ph -> -. A e. C )
2.1.12  Subclasses and subsets
Definition	df-ss 3013	Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3045). For a more traditional definition, but requiring a dummy variable, see dfss2 3015. Other possible definitions are given by dfss3 3016, ssequn1 3171, ssequn2 3174, and sseqin2 3220. (Contributed by NM, 27-Apr-1994.)
|- ( A C_ B <-> ( A i^i B ) = A )
Theorem	dfss 3014	Variant of subclass definition df-ss 3013. (Contributed by NM, 3-Sep-2004.)
|- ( A C_ B <-> A = ( A i^i B ) )
Theorem	dfss2 3015*	Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.)
|- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
Theorem	dfss3 3016*	Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)
|- ( A C_ B <-> A. x e. A x e. B )
Theorem	dfss2f 3017	Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 3-Jul-1994.) (Revised by Andrew Salmon, 27-Aug-2011.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
Theorem	dfss3f 3018	Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A C_ B <-> A. x e. A x e. B )
Theorem	nfss 3019	If x is not free in A and B, it is not free in A C_ B. (Contributed by NM, 27-Dec-1996.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A C_ B
Theorem	ssel 3020	Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.)
|- ( A C_ B -> ( C e. A -> C e. B ) )
Theorem	ssel2 3021	Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)
|- ( ( A C_ B /\ C e. A ) -> C e. B )
Theorem	sseli 3022	Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)
|- A C_ B   =>    |- ( C e. A -> C e. B )
Theorem	sselii 3023	Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.)
|- A C_ B   &    |- C e. A   =>    |- C e. B
Theorem	sseldi 3024	Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)
|- A C_ B   &    |- ( ph -> C e. A )   =>    |- ( ph -> C e. B )
Theorem	sseld 3025	Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.)
|- ( ph -> A C_ B )   =>    |- ( ph -> ( C e. A -> C e. B ) )
Theorem	sselda 3026	Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)
|- ( ph -> A C_ B )   =>    |- ( ( ph /\ C e. A ) -> C e. B )
Theorem	sseldd 3027	Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.)
|- ( ph -> A C_ B )   &    |- ( ph -> C e. A )   =>    |- ( ph -> C e. B )
Theorem	ssneld 3028	If a class is not in another class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A C_ B )   =>    |- ( ph -> ( -. C e. B -> -. C e. A ) )
Theorem	ssneldd 3029	If an element is not in a class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A C_ B )   &    |- ( ph -> -. C e. B )   =>    |- ( ph -> -. C e. A )
Theorem	ssriv 3030*	Inference based on subclass definition. (Contributed by NM, 5-Aug-1993.)
|- ( x e. A -> x e. B )   =>    |- A C_ B
Theorem	ssrd 3031	Deduction based on subclass definition. (Contributed by Thierry Arnoux, 8-Mar-2017.)
|- F/ x ph   &    |- F/_ x A   &    |- F/_ x B   &    |- ( ph -> ( x e. A -> x e. B ) )   =>    |- ( ph -> A C_ B )
Theorem	ssrdv 3032*	Deduction based on subclass definition. (Contributed by NM, 15-Nov-1995.)
|- ( ph -> ( x e. A -> x e. B ) )   =>    |- ( ph -> A C_ B )
Theorem	sstr2 3033	Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ( A C_ B -> ( B C_ C -> A C_ C ) )
Theorem	sstr 3034	Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)
|- ( ( A C_ B /\ B C_ C ) -> A C_ C )
Theorem	sstri 3035	Subclass transitivity inference. (Contributed by NM, 5-May-2000.)
|- A C_ B   &    |- B C_ C   =>    |- A C_ C
Theorem	sstrd 3036	Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)
|- ( ph -> A C_ B )   &    |- ( ph -> B C_ C )   =>    |- ( ph -> A C_ C )
Theorem	syl5ss 3037	Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)
|- A C_ B   &    |- ( ph -> B C_ C )   =>    |- ( ph -> A C_ C )
Theorem	syl6ss 3038	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> A C_ B )   &    |- B C_ C   =>    |- ( ph -> A C_ C )
Theorem	sylan9ss 3039	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 3040	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 3041	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 3042	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 3043	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 3044	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	ssid 3045	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 3046	Weakening of ssid 3045. (Contributed by BJ, 1-Sep-2022.)
|- ( ph -> A C_ A )
Theorem	ssv 3047	Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.)
|- A C_ _V
Theorem	sseq1 3048	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 3049	Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)
|- ( A = B -> ( C C_ A <-> C C_ B ) )
Theorem	sseq12 3050	Equality theorem for the subclass relationship. (Contributed by NM, 31-May-1999.)
|- ( ( A = B /\ C = D ) -> ( A C_ C <-> B C_ D ) )
Theorem	sseq1i 3051	An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.)
|- A = B   =>    |- ( A C_ C <-> B C_ C )
Theorem	sseq2i 3052	An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.)
|- A = B   =>    |- ( C C_ A <-> C C_ B )
Theorem	sseq12i 3053	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 3054	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 3055	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 3056	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 3057	Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.)
|- A = B   &    |- B C_ C   =>    |- A C_ C
Theorem	eqsstr3i 3058	Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.)
|- B = A   &    |- B C_ C   =>    |- A C_ C
Theorem	sseqtri 3059	Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.)
|- A C_ B   &    |- B = C   =>    |- A C_ C
Theorem	sseqtr4i 3060	Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)
|- A C_ B   &    |- C = B   =>    |- A C_ C
Theorem	eqsstrd 3061	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	eqsstr3d 3062	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 3063	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	sseqtr4d 3064	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 3065	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 3066	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 3067	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 3068	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 3069	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 3070	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	syl5eqss 3071	B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
|- A = B   &    |- ( ph -> B C_ C )   =>    |- ( ph -> A C_ C )
Theorem	syl5eqssr 3072	B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
|- B = A   &    |- ( ph -> B C_ C )   =>    |- ( ph -> A C_ C )
Theorem	syl6sseq 3073	A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
|- ( ph -> A C_ B )   &    |- B = C   =>    |- ( ph -> A C_ C )
Theorem	syl6sseqr 3074	A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
|- ( ph -> A C_ B )   &    |- C = B   =>    |- ( ph -> A C_ C )
Theorem	syl5sseq 3075	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- B C_ A   &    |- ( ph -> A = C )   =>    |- ( ph -> B C_ C )
Theorem	syl5sseqr 3076	Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- B C_ A   &    |- ( ph -> C = A )   =>    |- ( ph -> B C_ C )
Theorem	syl6eqss 3077	A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- ( ph -> A = B )   &    |- B C_ C   =>    |- ( ph -> A C_ C )
Theorem	syl6eqssr 3078	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 3079	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 3080	Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.)
|- ( B = A -> A C_ B )
Theorem	eqimssi 3081	Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.)
|- A = B   =>    |- A C_ B
Theorem	eqimss2i 3082	Infer subclass relationship from equality. (Contributed by NM, 7-Jan-2007.)
|- A = B   =>    |- B C_ A
Theorem	nssne1 3083	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 3084	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 3085*	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	ssralv 3086*	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 3087*	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 3088*	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 3089*	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 3090	Class abstractions in a subclass relationship. (Contributed by NM, 3-Jul-1994.)
|- ( { x | ph } C_ { x | ps } <-> A. x ( ph -> ps ) )
Theorem	abss 3091*	Class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.)
|- ( { x | ph } C_ A <-> A. x ( ph -> x e. A ) )
Theorem	ssab 3092*	Subclass of a class abstraction. (Contributed by NM, 16-Aug-2006.)
|- ( A C_ { x | ph } <-> A. x ( x e. A -> ph ) )
Theorem	ssabral 3093*	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 3094	Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.)
|- ( ph -> ps )   =>    |- { x | ph } C_ { x | ps }
Theorem	ss2abdv 3095*	Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> { x | ps } C_ { x | ch } )
Theorem	abssdv 3096*	Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
|- ( ph -> ( ps -> x e. A ) )   =>    |- ( ph -> { x | ps } C_ A )
Theorem	abssi 3097*	Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
|- ( ph -> x e. A )   =>    |- { x | ph } C_ A
Theorem	ss2rab 3098	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 3099*	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 3100*	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 ) )