Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



2.1.12 Subclasses and subsets


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



Theorem  dfss 2926 
Variant of subclass definition dfss 2925. (Contributed by NM,
3Sep2004.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  nssne1 2995 
Two classes are different if they don't include the same class.
(Contributed by NM, 23Apr2015.)



Theorem  nssne2 2996 
Two classes are different if they are not subclasses of the same class.
(Contributed by NM, 23Apr2015.)



Theorem  nssr 2997* 
Negation of subclass relationship. One direction of Exercise 13 of
[TakeutiZaring] p. 18.
(Contributed by Jim Kingdon, 15Jul2018.)



Theorem  ssralv 2998* 
Quantification restricted to a subclass. (Contributed by NM,
11Mar2006.)



Theorem  ssrexv 2999* 
Existential quantification restricted to a subclass. (Contributed by
NM, 11Jan2007.)



Theorem  ralss 3000* 
Restricted universal quantification on a subset in terms of superset.
(Contributed by Stefan O'Rear, 3Apr2015.)

