P. 30 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2901-3000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sbcth2 2901*	A substitution into a theorem. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Oct-2016.)
|- ( x e. B -> ph )   =>    |- ( A e. B -> [. A / x ]. ph )
Theorem	ra5 2902	Restricted quantifier version of Axiom 5 of [Mendelson] p. 69. This is an axiom of a predicate calculus for a restricted domain. Compare the unrestricted stdpc5 1516. (Contributed by NM, 16-Jan-2004.)
|- F/ x ph   =>    |- ( A. x e. A ( ph -> ps ) -> ( ph -> A. x e. A ps ) )
Theorem	rmo2ilem 2903*	Condition implying restricted "at most one." (Contributed by Jim Kingdon, 14-Jul-2018.)
|- F/ y ph   =>    |- ( E. y A. x e. A ( ph -> x = y ) -> E* x e. A ph )
Theorem	rmo2i 2904*	Condition implying restricted "at most one." (Contributed by NM, 17-Jun-2017.)
|- F/ y ph   =>    |- ( E. y e. A A. x e. A ( ph -> x = y ) -> E* x e. A ph )
Theorem	rmo3 2905*	Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
|- F/ y ph   =>    |- ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) )
Theorem	rmob 2906*	Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.)
|- ( x = B -> ( ph <-> ps ) )   &    |- ( x = C -> ( ph <-> ch ) )   =>    |- ( ( E* x e. A ph /\ ( B e. A /\ ps ) ) -> ( B = C <-> ( C e. A /\ ch ) ) )
Theorem	rmoi 2907*	Consequence of "at most one", using implicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
|- ( x = B -> ( ph <-> ps ) )   &    |- ( x = C -> ( ph <-> ch ) )   =>    |- ( ( E* x e. A ph /\ ( B e. A /\ ps ) /\ ( C e. A /\ ch ) ) -> B = C )
2.1.10  Proper substitution of classes for sets into classes
Syntax	csb 2908	Extend class notation to include the proper substitution of a class for a set into another class.
class [_ A / x ]_ B
Definition	df-csb 2909*	Define the proper substitution of a class for a set into another class. The underlined brackets distinguish it from the substitution into a wff, wsbc 2815, to prevent ambiguity. Theorem sbcel1g 2925 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2934 recreates substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.)
|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
Theorem	csb2 2910*	Alternate expression for the proper substitution into a class, without referencing substitution into a wff. Note that x can be free in B but cannot occur in A. (Contributed by NM, 2-Dec-2013.)
|- [_ A / x ]_ B = { y | E. x ( x = A /\ y e. B ) }
Theorem	csbeq1 2911	Analog of dfsbcq 2817 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
|- ( A = B -> [_ A / x ]_ C = [_ B / x ]_ C )
Theorem	cbvcsb 2912	Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on A. (Contributed by Jeff Hankins, 13-Sep-2009.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- F/_ y C   &    |- F/_ x D   &    |- ( x = y -> C = D )   =>    |- [_ A / x ]_ C = [_ A / y ]_ D
Theorem	cbvcsbv 2913*	Change the bound variable of a proper substitution into a class using implicit substitution. (Contributed by NM, 30-Sep-2008.) (Revised by Mario Carneiro, 13-Oct-2016.)
|- ( x = y -> B = C )   =>    |- [_ A / x ]_ B = [_ A / y ]_ C
Theorem	csbeq1d 2914	Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.)
|- ( ph -> A = B )   =>    |- ( ph -> [_ A / x ]_ C = [_ B / x ]_ C )
Theorem	csbid 2915	Analog of sbid 1697 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
|- [_ x / x ]_ A = A
Theorem	csbeq1a 2916	Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
|- ( x = A -> B = [_ A / x ]_ B )
Theorem	csbco 2917*	Composition law for chained substitutions into a class. (Contributed by NM, 10-Nov-2005.)
|- [_ A / y ]_ [_ y / x ]_ B = [_ A / x ]_ B
Theorem	csbtt 2918	Substitution doesn't affect a constant B (in which x is not free). (Contributed by Mario Carneiro, 14-Oct-2016.)
|- ( ( A e. V /\ F/_ x B ) -> [_ A / x ]_ B = B )
Theorem	csbconstgf 2919	Substitution doesn't affect a constant B (in which x is not free). (Contributed by NM, 10-Nov-2005.)
|- F/_ x B   =>    |- ( A e. V -> [_ A / x ]_ B = B )
Theorem	csbconstg 2920*	Substitution doesn't affect a constant B (in which x is not free). csbconstgf 2919 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.)
|- ( A e. V -> [_ A / x ]_ B = B )
Theorem	sbcel12g 2921	Distribute proper substitution through a membership relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ( A e. V -> ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. [_ A / x ]_ C ) )
Theorem	sbceqg 2922	Distribute proper substitution through an equality relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ( A e. V -> ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) )
Theorem	sbcnel12g 2923	Distribute proper substitution through negated membership. (Contributed by Andrew Salmon, 18-Jun-2011.)
|- ( A e. V -> ( [. A / x ]. B e/ C <-> [_ A / x ]_ B e/ [_ A / x ]_ C ) )
Theorem	sbcne12g 2924	Distribute proper substitution through an inequality. (Contributed by Andrew Salmon, 18-Jun-2011.)
|- ( A e. V -> ( [. A / x ]. B =/= C <-> [_ A / x ]_ B =/= [_ A / x ]_ C ) )
Theorem	sbcel1g 2925*	Move proper substitution in and out of a membership relation. Note that the scope of [. A / x ]. is the wff B e. C, whereas the scope of [_ A / x ]_ is the class B. (Contributed by NM, 10-Nov-2005.)
|- ( A e. V -> ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. C ) )
Theorem	sbceq1g 2926*	Move proper substitution to first argument of an equality. (Contributed by NM, 30-Nov-2005.)
|- ( A e. V -> ( [. A / x ]. B = C <-> [_ A / x ]_ B = C ) )
Theorem	sbcel2g 2927*	Move proper substitution in and out of a membership relation. (Contributed by NM, 14-Nov-2005.)
|- ( A e. V -> ( [. A / x ]. B e. C <-> B e. [_ A / x ]_ C ) )
Theorem	sbceq2g 2928*	Move proper substitution to second argument of an equality. (Contributed by NM, 30-Nov-2005.)
|- ( A e. V -> ( [. A / x ]. B = C <-> B = [_ A / x ]_ C ) )
Theorem	csbcomg 2929*	Commutative law for double substitution into a class. (Contributed by NM, 14-Nov-2005.)
|- ( ( A e. V /\ B e. W ) -> [_ A / x ]_ [_ B / y ]_ C = [_ B / y ]_ [_ A / x ]_ C )
Theorem	csbeq2d 2930	Formula-building deduction rule for class substitution. (Contributed by NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|- F/ x ph   &    |- ( ph -> B = C )   =>    |- ( ph -> [_ A / x ]_ B = [_ A / x ]_ C )
Theorem	csbeq2dv 2931*	Formula-building deduction rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|- ( ph -> B = C )   =>    |- ( ph -> [_ A / x ]_ B = [_ A / x ]_ C )
Theorem	csbeq2i 2932	Formula-building inference rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|- B = C   =>    |- [_ A / x ]_ B = [_ A / x ]_ C
Theorem	csbvarg 2933	The proper substitution of a class for setvar variable results in the class (if the class exists). (Contributed by NM, 10-Nov-2005.)
|- ( A e. V -> [_ A / x ]_ x = A )
Theorem	sbccsbg 2934*	Substitution into a wff expressed in terms of substitution into a class. (Contributed by NM, 15-Aug-2007.)
|- ( A e. V -> ( [. A / x ]. ph <-> y e. [_ A / x ]_ { y | ph } ) )
Theorem	sbccsb2g 2935	Substitution into a wff expressed in using substitution into a class. (Contributed by NM, 27-Nov-2005.)
|- ( A e. V -> ( [. A / x ]. ph <-> A e. [_ A / x ]_ { x | ph } ) )
Theorem	nfcsb1d 2936	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
|- ( ph -> F/_ x A )   =>    |- ( ph -> F/_ x [_ A / x ]_ B )
Theorem	nfcsb1 2937	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
|- F/_ x A   =>    |- F/_ x [_ A / x ]_ B
Theorem	nfcsb1v 2938*	Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.)
|- F/_ x [_ A / x ]_ B
Theorem	nfcsbd 2939	Deduction version of nfcsb 2940. (Contributed by NM, 21-Nov-2005.) (Revised by Mario Carneiro, 12-Oct-2016.)
|- F/ y ph   &    |- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/_ x [_ A / y ]_ B )
Theorem	nfcsb 2940	Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x [_ A / y ]_ B
Theorem	csbhypf 2941*	Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 2648 for class substitution version. (Contributed by NM, 19-Dec-2008.)
|- F/_ x A   &    |- F/_ x C   &    |- ( x = A -> B = C )   =>    |- ( y = A -> [_ y / x ]_ B = C )
Theorem	csbiebt 2942*	Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 2946.) (Contributed by NM, 11-Nov-2005.)
|- ( ( A e. V /\ F/_ x C ) -> ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )
Theorem	csbiedf 2943*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 13-Oct-2016.)
|- F/ x ph   &    |- ( ph -> F/_ x C )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x = A ) -> B = C )   =>    |- ( ph -> [_ A / x ]_ B = C )
Theorem	csbieb 2944*	Bidirectional conversion between an implicit class substitution hypothesis x = A -> B = C and its explicit substitution equivalent. (Contributed by NM, 2-Mar-2008.)
|- A e. _V   &    |- F/_ x C   =>    |- ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C )
Theorem	csbiebg 2945*	Bidirectional conversion between an implicit class substitution hypothesis x = A -> B = C and its explicit substitution equivalent. (Contributed by NM, 24-Mar-2013.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- F/_ x C   =>    |- ( A e. V -> ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )
Theorem	csbiegf 2946*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 11-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.)
|- ( A e. V -> F/_ x C )   &    |- ( x = A -> B = C )   =>    |- ( A e. V -> [_ A / x ]_ B = C )
Theorem	csbief 2947*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.)
|- A e. _V   &    |- F/_ x C   &    |- ( x = A -> B = C )   =>    |- [_ A / x ]_ B = C
Theorem	csbied 2948*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario Carneiro, 13-Oct-2016.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ x = A ) -> B = C )   =>    |- ( ph -> [_ A / x ]_ B = C )
Theorem	csbied2 2949*	Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- ( ph -> A e. V )   &    |- ( ph -> A = B )   &    |- ( ( ph /\ x = B ) -> C = D )   =>    |- ( ph -> [_ A / x ]_ C = D )
Theorem	csbie2t 2950*	Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 2951). (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 13-Oct-2016.)
|- A e. _V   &    |- B e. _V   =>    |- ( A. x A. y ( ( x = A /\ y = B ) -> C = D ) -> [_ A / x ]_ [_ B / y ]_ C = D )
Theorem	csbie2 2951*	Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 27-Aug-2007.)
|- A e. _V   &    |- B e. _V   &    |- ( ( x = A /\ y = B ) -> C = D )   =>    |- [_ A / x ]_ [_ B / y ]_ C = D
Theorem	csbie2g 2952*	Conversion of implicit substitution to explicit class substitution. This version of sbcie 2848 avoids a disjointness condition on x and A by substituting twice. (Contributed by Mario Carneiro, 11-Nov-2016.)
|- ( x = y -> B = C )   &    |- ( y = A -> C = D )   =>    |- ( A e. V -> [_ A / x ]_ B = D )
Theorem	sbcnestgf 2953	Nest the composition of two substitutions. (Contributed by Mario Carneiro, 11-Nov-2016.)
|- ( ( A e. V /\ A. y F/ x ph ) -> ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. ph ) )
Theorem	csbnestgf 2954	Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
|- ( ( A e. V /\ A. y F/_ x C ) -> [_ A / x ]_ [_ B / y ]_ C = [_ [_ A / x ]_ B / y ]_ C )
Theorem	sbcnestg 2955*	Nest the composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
|- ( A e. V -> ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. ph ) )
Theorem	csbnestg 2956*	Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
|- ( A e. V -> [_ A / x ]_ [_ B / y ]_ C = [_ [_ A / x ]_ B / y ]_ C )
Theorem	csbnest1g 2957	Nest the composition of two substitutions. (Contributed by NM, 23-May-2006.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
|- ( A e. V -> [_ A / x ]_ [_ B / x ]_ C = [_ [_ A / x ]_ B / x ]_ C )
Theorem	csbidmg 2958*	Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008.)
|- ( A e. V -> [_ A / x ]_ [_ A / x ]_ B = [_ A / x ]_ B )
Theorem	sbcco3g 2959*	Composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
|- ( x = A -> B = C )   =>    |- ( A e. V -> ( [. A / x ]. [. B / y ]. ph <-> [. C / y ]. ph ) )
Theorem	csbco3g 2960*	Composition of two class substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
|- ( x = A -> B = C )   =>    |- ( A e. V -> [_ A / x ]_ [_ B / y ]_ D = [_ C / y ]_ D )
Theorem	rspcsbela 2961*	Special case related to rspsbc 2896. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.)
|- ( ( A e. B /\ A. x e. B C e. D ) -> [_ A / x ]_ C e. D )
Theorem	sbnfc2 2962*	Two ways of expressing " x is (effectively) not free in A." (Contributed by Mario Carneiro, 14-Oct-2016.)
|- ( F/_ x A <-> A. y A. z [_ y / x ]_ A = [_ z / x ]_ A )
Theorem	csbabg 2963*	Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( A e. V -> [_ A / x ]_ { y | ph } = { y | [. A / x ]. ph } )
Theorem	cbvralcsf 2964	A more general version of cbvralf 2571 that doesn't require A and B to be distinct from x or y. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.)
|- F/_ y A   &    |- F/_ x B   &    |- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> A = B )   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x e. A ph <-> A. y e. B ps )
Theorem	cbvrexcsf 2965	A more general version of cbvrexf 2572 that has no distinct variable restrictions. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.) (Proof shortened by Mario Carneiro, 7-Dec-2014.)
|- F/_ y A   &    |- F/_ x B   &    |- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> A = B )   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x e. A ph <-> E. y e. B ps )
Theorem	cbvreucsf 2966	A more general version of cbvreuv 2579 that has no distinct variable rextrictions. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.)
|- F/_ y A   &    |- F/_ x B   &    |- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> A = B )   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E! x e. A ph <-> E! y e. B ps )
Theorem	cbvrabcsf 2967	A more general version of cbvrab 2599 with no distinct variable restrictions. (Contributed by Andrew Salmon, 13-Jul-2011.)
|- F/_ y A   &    |- F/_ x B   &    |- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> A = B )   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- { x e. A | ph } = { y e. B | ps }
Theorem	cbvralv2 2968*	Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.)
|- ( x = y -> ( ps <-> ch ) )   &    |- ( x = y -> A = B )   =>    |- ( A. x e. A ps <-> A. y e. B ch )
Theorem	cbvrexv2 2969*	Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.)
|- ( x = y -> ( ps <-> ch ) )   &    |- ( x = y -> A = B )   =>    |- ( E. x e. A ps <-> E. y e. B ch )
2.1.11  Define basic set operations and relations
Syntax	cdif 2970	Extend class notation to include class difference (read: " A minus B").
class ( A \ B )
Syntax	cun 2971	Extend class notation to include union of two classes (read: " A union B").
class ( A u. B )
Syntax	cin 2972	Extend class notation to include the intersection of two classes (read: " A intersect B").
class ( A i^i B )
Syntax	wss 2973	Extend wff notation to include the subclass relation. This is read " A is a subclass of B " or " B includes A." When A exists as a set, it is also read " A is a subset of B."
wff A C_ B
Theorem	difjust 2974*	Soundness justification theorem for df-dif 2975. (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 2975*	Define class difference, also called relative complement. Definition 5.12 of [TakeutiZaring] p. 20. Contrast this operation with union ( A u. B ) (df-un 2977) and intersection ( A i^i B ) (df-in 2979). 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 2976*	Soundness justification theorem for df-un 2977. (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 2977*	Define the union of two classes. Definition 5.6 of [TakeutiZaring] p. 16. Contrast this operation with difference ( A \ B ) (df-dif 2975) and intersection ( A i^i B ) (df-in 2979). (Contributed by NM, 23-Aug-1993.)
|- ( A u. B ) = { x | ( x e. A \/ x e. B ) }
Theorem	injust 2978*	Soundness justification theorem for df-in 2979. (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 2979*	Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. Contrast this operation with union ( A u. B ) (df-un 2977) and difference ( A \ B ) (df-dif 2975). (Contributed by NM, 29-Apr-1994.)
|- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
Theorem	dfin5 2980*	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 2981*	Alternate definition of class difference. (Contributed by NM, 25-Mar-2004.)
|- ( A \ B ) = { x e. A | -. x e. B }
Theorem	eldif 2982	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 2983	If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 2982. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. B )   &    |- ( ph -> -. A e. C )   =>    |- ( ph -> A e. ( B \ C ) )
Theorem	eldifad 2984	If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 2982. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. ( B \ C ) )   =>    |- ( ph -> A e. B )
Theorem	eldifbd 2985	If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 2982. (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 2986	Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that A C_ A (proved in ssid 3018). For a more traditional definition, but requiring a dummy variable, see dfss2 2988. Other possible definitions are given by dfss3 2989, ssequn1 3142, ssequn2 3145, and sseqin2 3185. (Contributed by NM, 27-Apr-1994.)
|- ( A C_ B <-> ( A i^i B ) = A )
Theorem	dfss 2987	Variant of subclass definition df-ss 2986. (Contributed by NM, 3-Sep-2004.)
|- ( A C_ B <-> A = ( A i^i B ) )
Theorem	dfss2 2988*	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 2989*	Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)
|- ( A C_ B <-> A. x e. A x e. B )
Theorem	dfss2f 2990	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 2991	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 2992	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 2993	Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.)
|- ( A C_ B -> ( C e. A -> C e. B ) )
Theorem	ssel2 2994	Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)
|- ( ( A C_ B /\ C e. A ) -> C e. B )
Theorem	sseli 2995	Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)
|- A C_ B   =>    |- ( C e. A -> C e. B )
Theorem	sselii 2996	Membership inference from subclass relationship. (Contributed by NM, 31-May-1999.)
|- A C_ B   &    |- C e. A   =>    |- C e. B
Theorem	sseldi 2997	Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)
|- A C_ B   &    |- ( ph -> C e. A )   =>    |- ( ph -> C e. B )
Theorem	sseld 2998	Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.)
|- ( ph -> A C_ B )   =>    |- ( ph -> ( C e. A -> C e. B ) )
Theorem	sselda 2999	Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)
|- ( ph -> A C_ B )   =>    |- ( ( ph /\ C e. A ) -> C e. B )
Theorem	sseldd 3000	Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.)
|- ( ph -> A C_ B )   &    |- ( ph -> C e. A )   =>    |- ( ph -> C e. B )