Type  Label  Description 
Statement 

Theorem  csbcomg 2901* 
Commutative law for double substitution into a class. (Contributed by
NM, 14Nov2005.)



Theorem  csbeq2d 2902 
Formulabuilding deduction rule for class substitution. (Contributed by
NM, 22Nov2005.) (Revised by Mario Carneiro, 1Sep2015.)



Theorem  csbeq2dv 2903* 
Formulabuilding deduction rule for class substitution. (Contributed by
NM, 10Nov2005.) (Revised by Mario Carneiro, 1Sep2015.)



Theorem  csbeq2i 2904 
Formulabuilding inference rule for class substitution. (Contributed by
NM, 10Nov2005.) (Revised by Mario Carneiro, 1Sep2015.)



Theorem  csbvarg 2905 
The proper substitution of a class for setvar variable results in the
class (if the class exists). (Contributed by NM, 10Nov2005.)



Theorem  sbccsbg 2906* 
Substitution into a wff expressed in terms of substitution into a class.
(Contributed by NM, 15Aug2007.)



Theorem  sbccsb2g 2907 
Substitution into a wff expressed in using substitution into a class.
(Contributed by NM, 27Nov2005.)



Theorem  nfcsb1d 2908 
Boundvariable hypothesis builder for substitution into a class.
(Contributed by Mario Carneiro, 12Oct2016.)



Theorem  nfcsb1 2909 
Boundvariable hypothesis builder for substitution into a class.
(Contributed by Mario Carneiro, 12Oct2016.)



Theorem  nfcsb1v 2910* 
Boundvariable hypothesis builder for substitution into a class.
(Contributed by NM, 17Aug2006.) (Revised by Mario Carneiro,
12Oct2016.)



Theorem  nfcsbd 2911 
Deduction version of nfcsb 2912. (Contributed by NM, 21Nov2005.)
(Revised by Mario Carneiro, 12Oct2016.)



Theorem  nfcsb 2912 
Boundvariable hypothesis builder for substitution into a class.
(Contributed by Mario Carneiro, 12Oct2016.)



Theorem  csbhypf 2913* 
Introduce an explicit substitution into an implicit substitution
hypothesis. See sbhypf 2620 for class substitution version. (Contributed
by NM, 19Dec2008.)



Theorem  csbiebt 2914* 
Conversion of implicit substitution to explicit substitution into a
class. (Closed theorem version of csbiegf 2918.) (Contributed by NM,
11Nov2005.)



Theorem  csbiedf 2915* 
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by Mario Carneiro, 13Oct2016.)



Theorem  csbieb 2916* 
Bidirectional conversion between an implicit class substitution
hypothesis and its explicit substitution equivalent.
(Contributed by NM, 2Mar2008.)



Theorem  csbiebg 2917* 
Bidirectional conversion between an implicit class substitution
hypothesis and its explicit substitution equivalent.
(Contributed by NM, 24Mar2013.) (Revised by Mario Carneiro,
11Dec2016.)



Theorem  csbiegf 2918* 
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by NM, 11Nov2005.) (Revised by Mario Carneiro,
13Oct2016.)



Theorem  csbief 2919* 
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by NM, 26Nov2005.) (Revised by Mario Carneiro,
13Oct2016.)



Theorem  csbied 2920* 
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by Mario Carneiro, 2Dec2014.) (Revised by Mario
Carneiro, 13Oct2016.)



Theorem  csbied2 2921* 
Conversion of implicit substitution to explicit class substitution,
deduction form. (Contributed by Mario Carneiro, 2Jan2017.)



Theorem  csbie2t 2922* 
Conversion of implicit substitution to explicit substitution into a
class (closed form of csbie2 2923). (Contributed by NM, 3Sep2007.)
(Revised by Mario Carneiro, 13Oct2016.)



Theorem  csbie2 2923* 
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by NM, 27Aug2007.)



Theorem  csbie2g 2924* 
Conversion of implicit substitution to explicit class substitution.
This version of sbcie 2820 avoids a disjointness condition on and
by
substituting twice. (Contributed by Mario Carneiro,
11Nov2016.)



Theorem  sbcnestgf 2925 
Nest the composition of two substitutions. (Contributed by Mario
Carneiro, 11Nov2016.)



Theorem  csbnestgf 2926 
Nest the composition of two substitutions. (Contributed by NM,
23Nov2005.) (Proof shortened by Mario Carneiro, 10Nov2016.)



Theorem  sbcnestg 2927* 
Nest the composition of two substitutions. (Contributed by NM,
27Nov2005.) (Proof shortened by Mario Carneiro, 11Nov2016.)



Theorem  csbnestg 2928* 
Nest the composition of two substitutions. (Contributed by NM,
23Nov2005.) (Proof shortened by Mario Carneiro, 10Nov2016.)



Theorem  csbnest1g 2929 
Nest the composition of two substitutions. (Contributed by NM,
23May2006.) (Proof shortened by Mario Carneiro, 11Nov2016.)



Theorem  csbidmg 2930* 
Idempotent law for class substitutions. (Contributed by NM,
1Mar2008.)



Theorem  sbcco3g 2931* 
Composition of two substitutions. (Contributed by NM, 27Nov2005.)
(Revised by Mario Carneiro, 11Nov2016.)



Theorem  csbco3g 2932* 
Composition of two class substitutions. (Contributed by NM,
27Nov2005.) (Revised by Mario Carneiro, 11Nov2016.)



Theorem  rspcsbela 2933* 
Special case related to rspsbc 2868. (Contributed by NM, 10Dec2005.)
(Proof shortened by Eric Schmidt, 17Jan2007.)



Theorem  sbnfc2 2934* 
Two ways of expressing " is (effectively) not free in ."
(Contributed by Mario Carneiro, 14Oct2016.)



Theorem  csbabg 2935* 
Move substitution into a class abstraction. (Contributed by NM,
13Dec2005.) (Proof shortened by Andrew Salmon, 9Jul2011.)



Theorem  cbvralcsf 2936 
A more general version of cbvralf 2544 that doesn't require and
to be distinct from or . Changes
bound variables using
implicit substitution. (Contributed by Andrew Salmon, 13Jul2011.)



Theorem  cbvrexcsf 2937 
A more general version of cbvrexf 2545 that has no distinct variable
restrictions. Changes bound variables using implicit substitution.
(Contributed by Andrew Salmon, 13Jul2011.) (Proof shortened by Mario
Carneiro, 7Dec2014.)



Theorem  cbvreucsf 2938 
A more general version of cbvreuv 2552 that has no distinct variable
rextrictions. Changes bound variables using implicit substitution.
(Contributed by Andrew Salmon, 13Jul2011.)



Theorem  cbvrabcsf 2939 
A more general version of cbvrab 2572 with no distinct variable
restrictions. (Contributed by Andrew Salmon, 13Jul2011.)



Theorem  cbvralv2 2940* 
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, 1May2017.)



Theorem  cbvrexv2 2941* 
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, 1May2017.)



2.1.11 Define basic set operations and
relations


Syntax  cdif 2942 
Extend class notation to include class difference (read: " minus
").



Syntax  cun 2943 
Extend class notation to include union of two classes (read: "
union ").



Syntax  cin 2944 
Extend class notation to include the intersection of two classes (read:
" intersect
").



Syntax  wss 2945 
Extend wff notation to include the subclass relation. This is
read " is a
subclass of " or
" includes ." When
exists as a set,
it is also read "
is a subset of ."



Syntax  wpss 2946 
Extend wff notation with proper subclass relation.



Theorem  difjust 2947* 
Soundness justification theorem for dfdif 2948. (Contributed by Rodolfo
Medina, 27Apr2010.) (Proof shortened by Andrew Salmon,
9Jul2011.)



Definition  dfdif 2948* 
Define class difference, also called relative complement. Definition
5.12 of [TakeutiZaring] p. 20.
Contrast this operation with union
(dfun 2950) and intersection (dfin 2952).
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 " excludes " to
mean . We will use " is removed from " to mean
i.e. the removal of an element or equivalently the
exclusion of a singleton. (Contributed by NM, 29Apr1994.)



Theorem  unjust 2949* 
Soundness justification theorem for dfun 2950. (Contributed by Rodolfo
Medina, 28Apr2010.) (Proof shortened by Andrew Salmon,
9Jul2011.)



Definition  dfun 2950* 
Define the union of two classes. Definition 5.6 of [TakeutiZaring]
p. 16. Contrast this operation with difference
(dfdif 2948) and intersection (dfin 2952). (Contributed
by NM, 23Aug1993.)



Theorem  injust 2951* 
Soundness justification theorem for dfin 2952. (Contributed by Rodolfo
Medina, 28Apr2010.) (Proof shortened by Andrew Salmon,
9Jul2011.)



Definition  dfin 2952* 
Define the intersection of two classes. Definition 5.6 of
[TakeutiZaring] p. 16. Contrast
this operation with union
(dfun 2950) and difference (dfdif 2948).
(Contributed by NM, 29Apr1994.)



Theorem  dfin5 2953* 
Alternate definition for the intersection of two classes. (Contributed
by NM, 6Jul2005.)



Theorem  dfdif2 2954* 
Alternate definition of class difference. (Contributed by NM,
25Mar2004.)



Theorem  eldif 2955 
Expansion of membership in a class difference. (Contributed by NM,
29Apr1994.)



Theorem  eldifd 2956 
If a class is in one class and not another, it is also in their
difference. Oneway deduction form of eldif 2955. (Contributed by David
Moews, 1May2017.)



Theorem  eldifad 2957 
If a class is in the difference of two classes, it is also in the
minuend. Oneway deduction form of eldif 2955. (Contributed by David
Moews, 1May2017.)



Theorem  eldifbd 2958 
If a class is in the difference of two classes, it is not in the
subtrahend. Oneway deduction form of eldif 2955. (Contributed by David
Moews, 1May2017.)



2.1.12 Subclasses and subsets


Definition  dfss 2959 
Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18.
Note that (proved in ssid 2992). Contrast this relationship with
the relationship
(as will be defined in dfpss 2961). For a more
traditional definition, but requiring a dummy variable, see dfss2 2962 (or
dfss3 2963 which is similar). (Contributed by NM,
27Apr1994.)



Theorem  dfss 2960 
Variant of subclass definition dfss 2959. (Contributed by NM,
3Sep2004.)



Definition  dfpss 2961 
Define proper subclass relationship between two classes. Definition 5.9
of [TakeutiZaring] p. 17. Note that
(proved in pssirr 3072).
Contrast this relationship with the relationship (as defined in
dfss 2959). Other possible definitions are given by dfpss2 3057 and
dfpss3 3058. (Contributed by NM, 7Feb1996.)



Theorem  dfss2 2962* 
Alternate definition of the subclass relationship between two classes.
Definition 5.9 of [TakeutiZaring]
p. 17. (Contributed by NM,
8Jan2002.)



Theorem  dfss3 2963* 
Alternate definition of subclass relationship. (Contributed by NM,
14Oct1999.)



Theorem  dfss2f 2964 
Equivalence for subclass relation, using boundvariable hypotheses
instead of distinct variable conditions. (Contributed by NM,
3Jul1994.) (Revised by Andrew Salmon, 27Aug2011.)



Theorem  dfss3f 2965 
Equivalence for subclass relation, using boundvariable hypotheses
instead of distinct variable conditions. (Contributed by NM,
20Mar2004.)



Theorem  nfss 2966 
If is not free in and , it is not free in .
(Contributed by NM, 27Dec1996.)



Theorem  ssel 2967 
Membership relationships follow from a subclass relationship.
(Contributed by NM, 5Aug1993.)



Theorem  ssel2 2968 
Membership relationships follow from a subclass relationship.
(Contributed by NM, 7Jun2004.)



Theorem  sseli 2969 
Membership inference from subclass relationship. (Contributed by NM,
5Aug1993.)



Theorem  sselii 2970 
Membership inference from subclass relationship. (Contributed by NM,
31May1999.)



Theorem  sseldi 2971 
Membership inference from subclass relationship. (Contributed by NM,
25Jun2014.)



Theorem  sseld 2972 
Membership deduction from subclass relationship. (Contributed by NM,
15Nov1995.)



Theorem  sselda 2973 
Membership deduction from subclass relationship. (Contributed by NM,
26Jun2014.)



Theorem  sseldd 2974 
Membership inference from subclass relationship. (Contributed by NM,
14Dec2004.)



Theorem  ssneld 2975 
If a class is not in another class, it is also not in a subclass of that
class. Deduction form. (Contributed by David Moews, 1May2017.)



Theorem  ssneldd 2976 
If an element is not in a class, it is also not in a subclass of that
class. Deduction form. (Contributed by David Moews, 1May2017.)



Theorem  ssriv 2977* 
Inference rule based on subclass definition. (Contributed by NM,
5Aug1993.)



Theorem  ssrd 2978 
Deduction rule based on subclass definition. (Contributed by Thierry
Arnoux, 8Mar2017.)



Theorem  ssrdv 2979* 
Deduction rule based on subclass definition. (Contributed by NM,
15Nov1995.)



Theorem  sstr2 2980 
Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17.
(Contributed by NM, 5Aug1993.) (Proof shortened by Andrew Salmon,
14Jun2011.)



Theorem  sstr 2981 
Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by
NM, 5Sep2003.)



Theorem  sstri 2982 
Subclass transitivity inference. (Contributed by NM, 5May2000.)



Theorem  sstrd 2983 
Subclass transitivity deduction. (Contributed by NM, 2Jun2004.)



Theorem  syl5ss 2984 
Subclass transitivity deduction. (Contributed by NM, 6Feb2014.)



Theorem  syl6ss 2985 
Subclass transitivity deduction. (Contributed by Jonathan BenNaim,
3Jun2011.)



Theorem  sylan9ss 2986 
A subclass transitivity deduction. (Contributed by NM, 27Sep2004.)
(Proof shortened by Andrew Salmon, 14Jun2011.)



Theorem  sylan9ssr 2987 
A subclass transitivity deduction. (Contributed by NM, 27Sep2004.)



Theorem  eqss 2988 
The subclass relationship is antisymmetric. Compare Theorem 4 of
[Suppes] p. 22. (Contributed by NM,
5Aug1993.)



Theorem  eqssi 2989 
Infer equality from two subclass relationships. Compare Theorem 4 of
[Suppes] p. 22. (Contributed by NM,
9Sep1993.)



Theorem  eqssd 2990 
Equality deduction from two subclass relationships. Compare Theorem 4
of [Suppes] p. 22. (Contributed by NM,
27Jun2004.)



Theorem  eqrd 2991 
Deduce equality of classes from equivalence of membership. (Contributed
by Thierry Arnoux, 21Mar2017.)



Theorem  ssid 2992 
Any class is a subclass of itself. Exercise 10 of [TakeutiZaring]
p. 18. (Contributed by NM, 5Aug1993.) (Proof shortened by Andrew
Salmon, 14Jun2011.)



Theorem  ssv 2993 
Any class is a subclass of the universal class. (Contributed by NM,
31Oct1995.)



Theorem  sseq1 2994 
Equality theorem for subclasses. (Contributed by NM, 5Aug1993.) (Proof
shortened by Andrew Salmon, 21Jun2011.)



Theorem  sseq2 2995 
Equality theorem for the subclass relationship. (Contributed by NM,
25Jun1998.)



Theorem  sseq12 2996 
Equality theorem for the subclass relationship. (Contributed by NM,
31May1999.)



Theorem  sseq1i 2997 
An equality inference for the subclass relationship. (Contributed by
NM, 18Aug1993.)



Theorem  sseq2i 2998 
An equality inference for the subclass relationship. (Contributed by
NM, 30Aug1993.)



Theorem  sseq12i 2999 
An equality inference for the subclass relationship. (Contributed by
NM, 31May1999.) (Proof shortened by Eric Schmidt, 26Jan2007.)



Theorem  sseq1d 3000 
An equality deduction for the subclass relationship. (Contributed by
NM, 14Aug1994.)

