Type  Label  Description 
Statement 

Theorem  nndcel 6301 
Set membership between two natural numbers is decidable. (Contributed by
Jim Kingdon, 6Sep2019.)

DECID


Theorem  nnsseleq 6302 
For natural numbers, inclusion is equivalent to membership or equality.
(Contributed by Jim Kingdon, 16Sep2021.)



Theorem  dcdifsnid 6303* 
If we remove a single element from a set with decidable equality then
put it back in, we end up with the original set. This strengthens
difsnss 3605 from subset to equality but the proof relies
on equality being
decidable. (Contributed by Jim Kingdon, 17Jun2022.)

DECID


Theorem  fnsnsplitdc 6304* 
Split a function into a single point and all the rest. (Contributed by
Stefan O'Rear, 27Feb2015.) (Revised by Jim Kingdon, 29Jan2023.)

DECID 

Theorem  funresdfunsndc 6305* 
Restricting a function to a domain without one element of the domain of
the function, and adding a pair of this element and the function value
of the element results in the function itself, where equality is
decidable. (Contributed by AV, 2Dec2018.) (Revised by Jim Kingdon,
30Jan2023.)

DECID


Theorem  nndifsnid 6306 
If we remove a single element from a natural number then put it back in,
we end up with the original natural number. This strengthens difsnss 3605
from subset to equality but the proof relies on equality being
decidable. (Contributed by Jim Kingdon, 31Aug2021.)



Theorem  nnaordi 6307 
Ordering property of addition. Proposition 8.4 of [TakeutiZaring]
p. 58, limited to natural numbers. (Contributed by NM, 3Feb1996.)
(Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnaord 6308 
Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58,
limited to natural numbers, and its converse. (Contributed by NM,
7Mar1996.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnaordr 6309 
Ordering property of addition of natural numbers. (Contributed by NM,
9Nov2002.)



Theorem  nnaword 6310 
Weak ordering property of addition. (Contributed by NM, 17Sep1995.)
(Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnacan 6311 
Cancellation law for addition of natural numbers. (Contributed by NM,
27Oct1995.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnaword1 6312 
Weak ordering property of addition. (Contributed by NM, 9Nov2002.)
(Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnaword2 6313 
Weak ordering property of addition. (Contributed by NM, 9Nov2002.)



Theorem  nnawordi 6314 
Adding to both sides of an inequality in (Contributed by Scott
Fenton, 16Apr2012.) (Revised by Mario Carneiro, 12May2012.)



Theorem  nnmordi 6315 
Ordering property of multiplication. Half of Proposition 8.19 of
[TakeutiZaring] p. 63, limited to
natural numbers. (Contributed by NM,
18Sep1995.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnmord 6316 
Ordering property of multiplication. Proposition 8.19 of [TakeutiZaring]
p. 63, limited to natural numbers. (Contributed by NM, 22Jan1996.)
(Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnmword 6317 
Weak ordering property of ordinal multiplication. (Contributed by Mario
Carneiro, 17Nov2014.)



Theorem  nnmcan 6318 
Cancellation law for multiplication of natural numbers. (Contributed by
NM, 26Oct1995.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  1onn 6319 
One is a natural number. (Contributed by NM, 29Oct1995.)



Theorem  2onn 6320 
The ordinal 2 is a natural number. (Contributed by NM, 28Sep2004.)



Theorem  3onn 6321 
The ordinal 3 is a natural number. (Contributed by Mario Carneiro,
5Jan2016.)



Theorem  4onn 6322 
The ordinal 4 is a natural number. (Contributed by Mario Carneiro,
5Jan2016.)



Theorem  nnm1 6323 
Multiply an element of by .
(Contributed by Mario
Carneiro, 17Nov2014.)



Theorem  nnm2 6324 
Multiply an element of by
(Contributed by Scott Fenton,
18Apr2012.) (Revised by Mario Carneiro, 17Nov2014.)



Theorem  nn2m 6325 
Multiply an element of by
(Contributed by Scott Fenton,
16Apr2012.) (Revised by Mario Carneiro, 17Nov2014.)



Theorem  nnaordex 6326* 
Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88.
(Contributed by NM, 5Dec1995.) (Revised by Mario Carneiro,
15Nov2014.)



Theorem  nnawordex 6327* 
Equivalence for weak ordering of natural numbers. (Contributed by NM,
8Nov2002.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnm00 6328 
The product of two natural numbers is zero iff at least one of them is
zero. (Contributed by Jim Kingdon, 11Nov2004.)



2.6.24 Equivalence relations and
classes


Syntax  wer 6329 
Extend the definition of a wff to include the equivalence predicate.



Syntax  cec 6330 
Extend the definition of a class to include equivalence class.



Syntax  cqs 6331 
Extend the definition of a class to include quotient set.



Definition  dfer 6332 
Define the equivalence relation predicate. Our notation is not standard.
A formal notation doesn't seem to exist in the literature; instead only
informal English tends to be used. The present definition, although
somewhat cryptic, nicely avoids dummy variables. In dfer2 6333 we derive a
more typical definition. We show that an equivalence relation is
reflexive, symmetric, and transitive in erref 6352, ersymb 6346, and ertr 6347.
(Contributed by NM, 4Jun1995.) (Revised by Mario Carneiro,
2Nov2015.)



Theorem  dfer2 6333* 
Alternate definition of equivalence predicate. (Contributed by NM,
3Jan1997.) (Revised by Mario Carneiro, 12Aug2015.)



Definition  dfec 6334 
Define the coset of
. Exercise 35 of [Enderton] p. 61. This
is called the equivalence class of modulo when is an
equivalence relation (i.e. when ; see dfer2 6333). In this case,
is a
representative (member) of the equivalence class ,
which contains all sets that are equivalent to . Definition of
[Enderton] p. 57 uses the notation (subscript) , although
we simply follow the brackets by since we don't have subscripted
expressions. For an alternate definition, see dfec2 6335. (Contributed by
NM, 23Jul1995.)



Theorem  dfec2 6335* 
Alternate definition of coset of .
Definition 34 of
[Suppes] p. 81. (Contributed by NM,
3Jan1997.) (Proof shortened by
Mario Carneiro, 9Jul2014.)



Theorem  ecexg 6336 
An equivalence class modulo a set is a set. (Contributed by NM,
24Jul1995.)



Theorem  ecexr 6337 
An inhabited equivalence class implies the representative is a set.
(Contributed by Mario Carneiro, 9Jul2014.)



Definition  dfqs 6338* 
Define quotient set.
is usually an equivalence relation.
Definition of [Enderton] p. 58.
(Contributed by NM, 23Jul1995.)



Theorem  ereq1 6339 
Equality theorem for equivalence predicate. (Contributed by NM,
4Jun1995.) (Revised by Mario Carneiro, 12Aug2015.)



Theorem  ereq2 6340 
Equality theorem for equivalence predicate. (Contributed by Mario
Carneiro, 12Aug2015.)



Theorem  errel 6341 
An equivalence relation is a relation. (Contributed by Mario Carneiro,
12Aug2015.)



Theorem  erdm 6342 
The domain of an equivalence relation. (Contributed by Mario Carneiro,
12Aug2015.)



Theorem  ercl 6343 
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12Aug2015.)



Theorem  ersym 6344 
An equivalence relation is symmetric. (Contributed by NM, 4Jun1995.)
(Revised by Mario Carneiro, 12Aug2015.)



Theorem  ercl2 6345 
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12Aug2015.)



Theorem  ersymb 6346 
An equivalence relation is symmetric. (Contributed by NM, 30Jul1995.)
(Revised by Mario Carneiro, 12Aug2015.)



Theorem  ertr 6347 
An equivalence relation is transitive. (Contributed by NM, 4Jun1995.)
(Revised by Mario Carneiro, 12Aug2015.)



Theorem  ertrd 6348 
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9Jul2014.)



Theorem  ertr2d 6349 
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9Jul2014.)



Theorem  ertr3d 6350 
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9Jul2014.)



Theorem  ertr4d 6351 
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9Jul2014.)



Theorem  erref 6352 
An equivalence relation is reflexive on its field. Compare Theorem 3M
of [Enderton] p. 56. (Contributed by
Mario Carneiro, 6May2013.)
(Revised by Mario Carneiro, 12Aug2015.)



Theorem  ercnv 6353 
The converse of an equivalence relation is itself. (Contributed by
Mario Carneiro, 12Aug2015.)



Theorem  errn 6354 
The range and domain of an equivalence relation are equal. (Contributed
by Rodolfo Medina, 11Oct2010.) (Revised by Mario Carneiro,
12Aug2015.)



Theorem  erssxp 6355 
An equivalence relation is a subset of the cartesian product of the field.
(Contributed by Mario Carneiro, 12Aug2015.)



Theorem  erex 6356 
An equivalence relation is a set if its domain is a set. (Contributed by
Rodolfo Medina, 15Oct2010.) (Proof shortened by Mario Carneiro,
12Aug2015.)



Theorem  erexb 6357 
An equivalence relation is a set if and only if its domain is a set.
(Contributed by Rodolfo Medina, 15Oct2010.) (Revised by Mario Carneiro,
12Aug2015.)



Theorem  iserd 6358* 
A reflexive, symmetric, transitive relation is an equivalence relation
on its domain. (Contributed by Mario Carneiro, 9Jul2014.) (Revised
by Mario Carneiro, 12Aug2015.)



Theorem  brdifun 6359 
Evaluate the incomparability relation. (Contributed by Mario Carneiro,
9Jul2014.)



Theorem  swoer 6360* 
Incomparability under a strict weak partial order is an equivalence
relation. (Contributed by Mario Carneiro, 9Jul2014.) (Revised by
Mario Carneiro, 12Aug2015.)



Theorem  swoord1 6361* 
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31Dec2014.)



Theorem  swoord2 6362* 
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31Dec2014.)



Theorem  eqerlem 6363* 
Lemma for eqer 6364. (Contributed by NM, 17Mar2008.) (Proof
shortened
by Mario Carneiro, 6Dec2016.)



Theorem  eqer 6364* 
Equivalence relation involving equality of dependent classes
and . (Contributed by NM, 17Mar2008.) (Revised by Mario
Carneiro, 12Aug2015.)



Theorem  ider 6365 
The identity relation is an equivalence relation. (Contributed by NM,
10May1998.) (Proof shortened by Andrew Salmon, 22Oct2011.) (Proof
shortened by Mario Carneiro, 9Jul2014.)



Theorem  0er 6366 
The empty set is an equivalence relation on the empty set. (Contributed
by Mario Carneiro, 5Sep2015.)



Theorem  eceq1 6367 
Equality theorem for equivalence class. (Contributed by NM,
23Jul1995.)



Theorem  eceq1d 6368 
Equality theorem for equivalence class (deduction form). (Contributed
by Jim Kingdon, 31Dec2019.)



Theorem  eceq2 6369 
Equality theorem for equivalence class. (Contributed by NM,
23Jul1995.)



Theorem  elecg 6370 
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by Mario Carneiro, 9Jul2014.)



Theorem  elec 6371 
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by NM, 23Jul1995.)



Theorem  relelec 6372 
Membership in an equivalence class when is a relation. (Contributed
by Mario Carneiro, 11Sep2015.)



Theorem  ecss 6373 
An equivalence class is a subset of the domain. (Contributed by NM,
6Aug1995.) (Revised by Mario Carneiro, 12Aug2015.)



Theorem  ecdmn0m 6374* 
A representative of an inhabited equivalence class belongs to the domain
of the equivalence relation. (Contributed by Jim Kingdon,
21Aug2019.)



Theorem  ereldm 6375 
Equality of equivalence classes implies equivalence of domain
membership. (Contributed by NM, 28Jan1996.) (Revised by Mario
Carneiro, 12Aug2015.)



Theorem  erth 6376 
Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82.
(Contributed by NM, 23Jul1995.) (Revised by Mario Carneiro,
6Jul2015.)



Theorem  erth2 6377 
Basic property of equivalence relations. Compare Theorem 73 of [Suppes]
p. 82. Assumes membership of the second argument in the domain.
(Contributed by NM, 30Jul1995.) (Revised by Mario Carneiro,
6Jul2015.)



Theorem  erthi 6378 
Basic property of equivalence relations. Part of Lemma 3N of [Enderton]
p. 57. (Contributed by NM, 30Jul1995.) (Revised by Mario Carneiro,
9Jul2014.)



Theorem  ecidsn 6379 
An equivalence class modulo the identity relation is a singleton.
(Contributed by NM, 24Oct2004.)



Theorem  qseq1 6380 
Equality theorem for quotient set. (Contributed by NM, 23Jul1995.)



Theorem  qseq2 6381 
Equality theorem for quotient set. (Contributed by NM, 23Jul1995.)



Theorem  elqsg 6382* 
Closed form of elqs 6383. (Contributed by Rodolfo Medina,
12Oct2010.)



Theorem  elqs 6383* 
Membership in a quotient set. (Contributed by NM, 23Jul1995.)



Theorem  elqsi 6384* 
Membership in a quotient set. (Contributed by NM, 23Jul1995.)



Theorem  ecelqsg 6385 
Membership of an equivalence class in a quotient set. (Contributed by
Jeff Madsen, 10Jun2010.) (Revised by Mario Carneiro, 9Jul2014.)



Theorem  ecelqsi 6386 
Membership of an equivalence class in a quotient set. (Contributed by
NM, 25Jul1995.) (Revised by Mario Carneiro, 9Jul2014.)



Theorem  ecopqsi 6387 
"Closure" law for equivalence class of ordered pairs. (Contributed
by
NM, 25Mar1996.)



Theorem  qsexg 6388 
A quotient set exists. (Contributed by FL, 19May2007.) (Revised by
Mario Carneiro, 9Jul2014.)



Theorem  qsex 6389 
A quotient set exists. (Contributed by NM, 14Aug1995.)



Theorem  uniqs 6390 
The union of a quotient set. (Contributed by NM, 9Dec2008.)



Theorem  qsss 6391 
A quotient set is a set of subsets of the base set. (Contributed by
Mario Carneiro, 9Jul2014.) (Revised by Mario Carneiro,
12Aug2015.)



Theorem  uniqs2 6392 
The union of a quotient set. (Contributed by Mario Carneiro,
11Jul2014.)



Theorem  snec 6393 
The singleton of an equivalence class. (Contributed by NM,
29Jan1999.) (Revised by Mario Carneiro, 9Jul2014.)



Theorem  ecqs 6394 
Equivalence class in terms of quotient set. (Contributed by NM,
29Jan1999.)



Theorem  ecid 6395 
A set is equal to its converse epsilon coset. (Note: converse epsilon
is not an equivalence relation.) (Contributed by NM, 13Aug1995.)
(Revised by Mario Carneiro, 9Jul2014.)



Theorem  ecidg 6396 
A set is equal to its converse epsilon coset. (Note: converse epsilon
is not an equivalence relation.) (Contributed by Jim Kingdon,
8Jan2020.)



Theorem  qsid 6397 
A set is equal to its quotient set mod converse epsilon. (Note:
converse epsilon is not an equivalence relation.) (Contributed by NM,
13Aug1995.) (Revised by Mario Carneiro, 9Jul2014.)



Theorem  ectocld 6398* 
Implicit substitution of class for equivalence class. (Contributed by
Mario Carneiro, 9Jul2014.)



Theorem  ectocl 6399* 
Implicit substitution of class for equivalence class. (Contributed by
NM, 23Jul1995.) (Revised by Mario Carneiro, 9Jul2014.)



Theorem  elqsn0m 6400* 
An element of a quotient set is inhabited. (Contributed by Jim Kingdon,
21Aug2019.)

