Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



Theorem  cbvrexcsf 2909 
A more general version of cbvrexf 2528 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 2910 
A more general version of cbvreuv 2535 that has no distinct variable
rextrictions. Changes bound variables using implicit substitution.
(Contributed by Andrew Salmon, 13Jul2011.)



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



Theorem  cbvralv2 2912* 
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 2913* 
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 2914 
Extend class notation to include class difference (read: " minus
").



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



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



Syntax  wss 2917 
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 2918 
Extend wff notation with proper subclass relation.



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



Definition  dfdif 2920* 
Define class difference, also called relative complement. Definition
5.12 of [TakeutiZaring] p. 20.
Contrast this operation with union
(dfun 2922) and intersection (dfin 2924).
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 2921* 
Soundness justification theorem for dfun 2922. (Contributed by Rodolfo
Medina, 28Apr2010.) (Proof shortened by Andrew Salmon,
9Jul2011.)



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



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



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



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



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



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



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



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



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



2.1.12 Subclasses and subsets


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



Theorem  dfss 2932 
Variant of subclass definition dfss 2931. (Contributed by NM,
3Sep2004.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  ssneld 2947 
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 2948 
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 2949* 
Inference rule based on subclass definition. (Contributed by NM,
5Aug1993.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  ssid 2964 
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 2965 
Any class is a subclass of the universal class. (Contributed by NM,
31Oct1995.)



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



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



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



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



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



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



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



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



Theorem  sseq12d 2974 
An equality deduction for the subclass relationship. (Contributed by
NM, 31May1999.)



Theorem  eqsstri 2975 
Substitution of equality into a subclass relationship. (Contributed by
NM, 16Jul1995.)



Theorem  eqsstr3i 2976 
Substitution of equality into a subclass relationship. (Contributed by
NM, 19Oct1999.)



Theorem  sseqtri 2977 
Substitution of equality into a subclass relationship. (Contributed by
NM, 28Jul1995.)



Theorem  sseqtr4i 2978 
Substitution of equality into a subclass relationship. (Contributed by
NM, 4Apr1995.)



Theorem  eqsstrd 2979 
Substitution of equality into a subclass relationship. (Contributed by
NM, 25Apr2004.)



Theorem  eqsstr3d 2980 
Substitution of equality into a subclass relationship. (Contributed by
NM, 25Apr2004.)



Theorem  sseqtrd 2981 
Substitution of equality into a subclass relationship. (Contributed by
NM, 25Apr2004.)



Theorem  sseqtr4d 2982 
Substitution of equality into a subclass relationship. (Contributed by
NM, 25Apr2004.)



Theorem  3sstr3i 2983 
Substitution of equality in both sides of a subclass relationship.
(Contributed by NM, 13Jan1996.) (Proof shortened by Eric Schmidt,
26Jan2007.)



Theorem  3sstr4i 2984 
Substitution of equality in both sides of a subclass relationship.
(Contributed by NM, 13Jan1996.) (Proof shortened by Eric Schmidt,
26Jan2007.)



Theorem  3sstr3g 2985 
Substitution of equality into both sides of a subclass relationship.
(Contributed by NM, 1Oct2000.)



Theorem  3sstr4g 2986 
Substitution of equality into both sides of a subclass relationship.
(Contributed by NM, 16Aug1994.) (Proof shortened by Eric Schmidt,
26Jan2007.)



Theorem  3sstr3d 2987 
Substitution of equality into both sides of a subclass relationship.
(Contributed by NM, 1Oct2000.)



Theorem  3sstr4d 2988 
Substitution of equality into both sides of a subclass relationship.
(Contributed by NM, 30Nov1995.) (Proof shortened by Eric Schmidt,
26Jan2007.)



Theorem  syl5eqss 2989 
B chained subclass and equality deduction. (Contributed by NM,
25Apr2004.)



Theorem  syl5eqssr 2990 
B chained subclass and equality deduction. (Contributed by NM,
25Apr2004.)



Theorem  syl6sseq 2991 
A chained subclass and equality deduction. (Contributed by NM,
25Apr2004.)



Theorem  syl6sseqr 2992 
A chained subclass and equality deduction. (Contributed by NM,
25Apr2004.)



Theorem  syl5sseq 2993 
Subclass transitivity deduction. (Contributed by Jonathan BenNaim,
3Jun2011.)



Theorem  syl5sseqr 2994 
Subclass transitivity deduction. (Contributed by Jonathan BenNaim,
3Jun2011.)



Theorem  syl6eqss 2995 
A chained subclass and equality deduction. (Contributed by Mario
Carneiro, 2Jan2017.)



Theorem  syl6eqssr 2996 
A chained subclass and equality deduction. (Contributed by Mario
Carneiro, 2Jan2017.)



Theorem  eqimss 2997 
Equality implies the subclass relation. (Contributed by NM, 5Aug1993.)
(Proof shortened by Andrew Salmon, 21Jun2011.)



Theorem  eqimss2 2998 
Equality implies the subclass relation. (Contributed by NM,
23Nov2003.)



Theorem  eqimssi 2999 
Infer subclass relationship from equality. (Contributed by NM,
6Jan2007.)



Theorem  eqimss2i 3000 
Infer subclass relationship from equality. (Contributed by NM,
7Jan2007.)

