Type  Label  Description 
Statement 

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



Theorem  cbvralv2 3202* 
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 3203* 
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.10 Define boolean set
operations


Syntax  cnin 3204 
Extend class notation to include antiintersection (read: "the
antiintersection of and ").

&ncap 

Syntax  ccompl 3205 
Extend class notation to include complement. (read: "the complement of
" ).

∼ 

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



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



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



Syntax  csymdif 3209 
Extend class notation to include the symmetric difference of two
classes.



Theorem  ninjust 3210* 
Soundness theorem for dfnin 3211. (Contributed by SF, 10Jan2015.)



Definition  dfnin 3211* 
Define the antiintersection of two classes. This operation is used
implicitly after Axiom P1 of [Hailperin] p. 6, though there does not
seem to be any notation for it in the literature. (Contributed by SF,
10Jan2015.)

&ncap


Definition  dfcompl 3212 
Define the complement of a class. Compare nicdfneg 1435. (Contributed by
SF, 10Jan2015.)

∼
&ncap 

Definition  dfin 3213 
Define the intersection of two classes. See elin 3219
for membership.
(Contributed by SF, 10Jan2015.)

∼ &ncap 

Definition  dfun 3214 
Define the union of two classes. See elun 3220 for membership. (Contributed
by SF, 10Jan2015.)

∼ &ncap ∼ 

Definition  dfdif 3215 
Define the difference of two classes. See eldif 3221 for membership.
(Contributed by SF, 10Jan2015.)

∼ 

Definition  dfsymdif 3216 
Define the symmetric difference of two classes. Definition IX.9.10,
[Rosser] p. 238. (Contributed by SF,
10Jan2015.)



Theorem  elning 3217 
Membership in antiintersection. (Contributed by SF, 10Jan2015.)

&ncap 

Theorem  elcomplg 3218 
Membership in class complement. (Contributed by SF, 10Jan2015.)

∼ 

Theorem  elin 3219 
Membership in intersection. (Contributed by SF, 10Jan2015.)



Theorem  elun 3220 
Membership in union. (Contributed by SF, 10Jan2015.)



Theorem  eldif 3221 
Membership in difference. (Contributed by SF, 10Jan2015.)



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



Theorem  elsymdif 3223 
Membership in symmetric difference. (Contributed by SF, 10Jan2015.)



Theorem  elnin 3224 
Membership in antiintersection. (Contributed by SF, 10Jan2015.)

&ncap 

Theorem  elcompl 3225 
Membership in complement. (Contributed by SF, 10Jan2015.)

∼ 

Theorem  nincom 3226 
Antiintersection commutes. (Contributed by SF, 10Jan2015.)

&ncap
&ncap


Theorem  dblcompl 3227 
Double complement law. (Contributed by SF, 10Jan2015.)

∼ ∼ 

Theorem  nfnin 3228 
Hypothesis builder for antiintersection. (Contributed by SF,
2Jan2018.)

&ncap 

Theorem  nfcompl 3229 
Hypothesis builder for complement. (Contributed by SF, 2Jan2018.)

∼ 

Theorem  nfin 3230 
Hypothesis builder for intersection. (Contributed by SF,
2Jan2018.)



Theorem  nfun 3231 
Hypothesis builder for union. (Contributed by SF, 2Jan2018.)



Theorem  nfdif 3232 
Hypothesis builder for difference. (Contributed by SF, 2Jan2018.)



Theorem  nfsymdif 3233 
Hypothesis builder for symmetric difference. (Contributed by SF,
2Jan2018.)



Theorem  nineq1 3234 
Equality law for antiintersection. (Contributed by SF,
11Jan2015.)

&ncap
&ncap


Theorem  nineq2 3235 
Equality law for antiintersection. (Contributed by SF, 11Jan2015.)

&ncap
&ncap


Theorem  nineq12 3236 
Equality law for antiintersection. (Contributed by SF, 11Jan2015.)

&ncap
&ncap 

Theorem  nineq1i 3237 
Equality inference for antiintersection. (Contributed by SF,
11Jan2015.)

&ncap
&ncap


Theorem  nineq2i 3238 
Equality inference for antiintersection. (Contributed by SF,
11Jan2015.)

&ncap
&ncap


Theorem  nineq12i 3239 
Equality inference for antiintersection. (Contributed by SF,
11Jan2015.)

&ncap
&ncap


Theorem  nineq1d 3240 
Equality deduction for antiintersection. (Contributed by SF,
11Jan2015.)

&ncap &ncap 

Theorem  nineq2d 3241 
Equality deduction for antiintersection. (Contributed by SF,
11Jan2015.)

&ncap &ncap 

Theorem  nineq12d 3242 
Equality inference for antiintersection. (Contributed by SF,
11Jan2015.)

&ncap &ncap 

Theorem  compleq 3243 
Equality law for complement. (Contributed by SF, 11Jan2015.)

∼ ∼


Theorem  compleqi 3244 
Equality inference for complement. (Contributed by SF, 11Jan2015.)

∼
∼ 

Theorem  compleqd 3245 
Equality deduction for complement. (Contributed by SF, 11Jan2015.)

∼ ∼ 

Theorem  difeq1 3246 
Equality theorem for class difference. (Contributed by NM, 10Feb1997.)
(Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  difeq2 3247 
Equality theorem for class difference. (Contributed by NM, 10Feb1997.)
(Proof shortened by Andrew Salmon, 26Jun2011.)



Theorem  symdifeq1 3248 
Equality law for intersection. (Contributed by SF, 11Jan2015.)



Theorem  symdifeq2 3249 
Equality law for intersection. (Contributed by SF, 11Jan2015.)



Theorem  symdifeq12 3250 
Equality law for intersection. (Contributed by SF, 11Jan2015.)



Theorem  symdifeq1i 3251 
Equality inference for symmetric difference. (Contributed by SF,
11Jan2015.)



Theorem  symdifeq2i 3252 
Equality inference for symmetric difference. (Contributed by SF,
11Jan2015.)



Theorem  symdifeq12i 3253 
Equality inference for symmetric difference. (Contributed by SF,
11Jan2015.)



Theorem  symdifeq1d 3254 
Equality deduction for symmetric difference. (Contributed by SF,
11Jan2015.)



Theorem  symdifeq2d 3255 
Equality deduction for symmetric difference. (Contributed by SF,
11Jan2015.)



Theorem  symdifeq12d 3256 
Equality inference for symmetric difference. (Contributed by SF,
11Jan2015.)



2.1.11 Subclasses and subsets


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



Definition  dfss 3259 
Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18.
For example,
1 , 2 1 , 2 , 3 (exss in set.mm).
Note that (proved in ssid 3290). Contrast this relationship with
the relationship
(as will be defined
in dfpss 3261). For a more
traditional definition, but requiring a dummy variable, see dfss2 3262.
Other possible definitions are given by dfss3 3263, dfss4 3489, sspss 3368,
ssequn1 3433, ssequn2 3436, sseqin2 3474, and ssdif0 3609. (Contributed by NM,
27Apr1994.)



Theorem  dfss 3260 
Variant of subclass definition dfss 3259. (Contributed by NM,
3Sep2004.)



Definition  dfpss 3261 
Define proper subclass relationship between two classes. Definition 5.9
of [TakeutiZaring] p. 17. For
example, 1 , 2
1 , 2 , 3
(expss in
set.mm). Note that (proved in pssirr 3369).
Contrast this relationship with the relationship (as defined in
dfss 3259). Other possible definitions are given by dfpss2 3354 and
dfpss3 3355. (Contributed by NM, 7Feb1996.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

