Theorem List for Intuitionistic Logic Explorer - 6401-6500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ecexg 6401 |
An equivalence class modulo a set is a set. (Contributed by NM,
24-Jul-1995.)
|
|
|
Theorem | ecexr 6402 |
An inhabited equivalence class implies the representative is a set.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
|
|
Definition | df-qs 6403* |
Define quotient set.
is usually an equivalence relation.
Definition of [Enderton] p. 58.
(Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | ereq1 6404 |
Equality theorem for equivalence predicate. (Contributed by NM,
4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ereq2 6405 |
Equality theorem for equivalence predicate. (Contributed by Mario
Carneiro, 12-Aug-2015.)
|
|
|
Theorem | errel 6406 |
An equivalence relation is a relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
|
|
Theorem | erdm 6407 |
The domain of an equivalence relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
|
|
Theorem | ercl 6408 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ersym 6409 |
An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ercl2 6410 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ersymb 6411 |
An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ertr 6412 |
An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ertrd 6413 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ertr2d 6414 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ertr3d 6415 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ertr4d 6416 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
|
|
Theorem | erref 6417 |
An equivalence relation is reflexive on its field. Compare Theorem 3M
of [Enderton] p. 56. (Contributed by
Mario Carneiro, 6-May-2013.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ercnv 6418 |
The converse of an equivalence relation is itself. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | errn 6419 |
The range and domain of an equivalence relation are equal. (Contributed
by Rodolfo Medina, 11-Oct-2010.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
|
|
Theorem | erssxp 6420 |
An equivalence relation is a subset of the cartesian product of the field.
(Contributed by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | erex 6421 |
An equivalence relation is a set if its domain is a set. (Contributed by
Rodolfo Medina, 15-Oct-2010.) (Proof shortened by Mario Carneiro,
12-Aug-2015.)
|
|
|
Theorem | erexb 6422 |
An equivalence relation is a set if and only if its domain is a set.
(Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
|
|
Theorem | iserd 6423* |
A reflexive, symmetric, transitive relation is an equivalence relation
on its domain. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised
by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | brdifun 6424 |
Evaluate the incomparability relation. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
|
|
Theorem | swoer 6425* |
Incomparability under a strict weak partial order is an equivalence
relation. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by
Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | swoord1 6426* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
|
|
Theorem | swoord2 6427* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
|
|
Theorem | eqerlem 6428* |
Lemma for eqer 6429. (Contributed by NM, 17-Mar-2008.) (Proof
shortened
by Mario Carneiro, 6-Dec-2016.)
|
|
|
Theorem | eqer 6429* |
Equivalence relation involving equality of dependent classes
and . (Contributed by NM, 17-Mar-2008.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ider 6430 |
The identity relation is an equivalence relation. (Contributed by NM,
10-May-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Proof
shortened by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | 0er 6431 |
The empty set is an equivalence relation on the empty set. (Contributed
by Mario Carneiro, 5-Sep-2015.)
|
|
|
Theorem | eceq1 6432 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
|
|
Theorem | eceq1d 6433 |
Equality theorem for equivalence class (deduction form). (Contributed
by Jim Kingdon, 31-Dec-2019.)
|
|
|
Theorem | eceq2 6434 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
|
|
Theorem | elecg 6435 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | elec 6436 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | relelec 6437 |
Membership in an equivalence class when is a relation. (Contributed
by Mario Carneiro, 11-Sep-2015.)
|
|
|
Theorem | ecss 6438 |
An equivalence class is a subset of the domain. (Contributed by NM,
6-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ecdmn0m 6439* |
A representative of an inhabited equivalence class belongs to the domain
of the equivalence relation. (Contributed by Jim Kingdon,
21-Aug-2019.)
|
|
|
Theorem | ereldm 6440 |
Equality of equivalence classes implies equivalence of domain
membership. (Contributed by NM, 28-Jan-1996.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
|
|
Theorem | erth 6441 |
Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82.
(Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro,
6-Jul-2015.)
|
|
|
Theorem | erth2 6442 |
Basic property of equivalence relations. Compare Theorem 73 of [Suppes]
p. 82. Assumes membership of the second argument in the domain.
(Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro,
6-Jul-2015.)
|
|
|
Theorem | erthi 6443 |
Basic property of equivalence relations. Part of Lemma 3N of [Enderton]
p. 57. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro,
9-Jul-2014.)
|
|
|
Theorem | ecidsn 6444 |
An equivalence class modulo the identity relation is a singleton.
(Contributed by NM, 24-Oct-2004.)
|
|
|
Theorem | qseq1 6445 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | qseq2 6446 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | elqsg 6447* |
Closed form of elqs 6448. (Contributed by Rodolfo Medina,
12-Oct-2010.)
|
|
|
Theorem | elqs 6448* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | elqsi 6449* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | ecelqsg 6450 |
Membership of an equivalence class in a quotient set. (Contributed by
Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ecelqsi 6451 |
Membership of an equivalence class in a quotient set. (Contributed by
NM, 25-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ecopqsi 6452 |
"Closure" law for equivalence class of ordered pairs. (Contributed
by
NM, 25-Mar-1996.)
|
|
|
Theorem | qsexg 6453 |
A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by
Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | qsex 6454 |
A quotient set exists. (Contributed by NM, 14-Aug-1995.)
|
|
|
Theorem | uniqs 6455 |
The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
|
|
|
Theorem | qsss 6456 |
A quotient set is a set of subsets of the base set. (Contributed by
Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
|
|
Theorem | uniqs2 6457 |
The union of a quotient set. (Contributed by Mario Carneiro,
11-Jul-2014.)
|
|
|
Theorem | snec 6458 |
The singleton of an equivalence class. (Contributed by NM,
29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ecqs 6459 |
Equivalence class in terms of quotient set. (Contributed by NM,
29-Jan-1999.)
|
|
|
Theorem | ecid 6460 |
A set is equal to its converse epsilon coset. (Note: converse epsilon
is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ecidg 6461 |
A set is equal to its converse epsilon coset. (Note: converse epsilon
is not an equivalence relation.) (Contributed by Jim Kingdon,
8-Jan-2020.)
|
|
|
Theorem | qsid 6462 |
A set is equal to its quotient set mod converse epsilon. (Note:
converse epsilon is not an equivalence relation.) (Contributed by NM,
13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ectocld 6463* |
Implicit substitution of class for equivalence class. (Contributed by
Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ectocl 6464* |
Implicit substitution of class for equivalence class. (Contributed by
NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | elqsn0m 6465* |
An element of a quotient set is inhabited. (Contributed by Jim Kingdon,
21-Aug-2019.)
|
|
|
Theorem | elqsn0 6466 |
A quotient set doesn't contain the empty set. (Contributed by NM,
24-Aug-1995.)
|
|
|
Theorem | ecelqsdm 6467 |
Membership of an equivalence class in a quotient set. (Contributed by
NM, 30-Jul-1995.)
|
|
|
Theorem | xpider 6468 |
A square Cartesian product is an equivalence relation (in general it's not
a poset). (Contributed by FL, 31-Jul-2009.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
|
|
Theorem | iinerm 6469* |
The intersection of a nonempty family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
|
|
Theorem | riinerm 6470* |
The relative intersection of a family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
|
|
Theorem | erinxp 6471 |
A restricted equivalence relation is an equivalence relation.
(Contributed by Mario Carneiro, 10-Jul-2015.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ecinxp 6472 |
Restrict the relation in an equivalence class to a base set. (Contributed
by Mario Carneiro, 10-Jul-2015.)
|
|
|
Theorem | qsinxp 6473 |
Restrict the equivalence relation in a quotient set to the base set.
(Contributed by Mario Carneiro, 23-Feb-2015.)
|
|
|
Theorem | qsel 6474 |
If an element of a quotient set contains a given element, it is equal to
the equivalence class of the element. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
|
|
Theorem | qliftlem 6475* |
, a function lift, is
a subset of . (Contributed by
Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftrel 6476* |
, a function lift, is
a subset of . (Contributed by
Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftel 6477* |
Elementhood in the relation . (Contributed by Mario Carneiro,
23-Dec-2016.)
|
|
|
Theorem | qliftel1 6478* |
Elementhood in the relation . (Contributed by Mario Carneiro,
23-Dec-2016.)
|
|
|
Theorem | qliftfun 6479* |
The function is the
unique function defined by
, provided that the well-definedness condition
holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftfund 6480* |
The function is the
unique function defined by
, provided that the well-definedness condition
holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftfuns 6481* |
The function is the
unique function defined by
, provided that the well-definedness condition
holds.
(Contributed by Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftf 6482* |
The domain and range of the function . (Contributed by Mario
Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftval 6483* |
The value of the function . (Contributed by Mario Carneiro,
23-Dec-2016.)
|
|
|
Theorem | ecoptocl 6484* |
Implicit substitution of class for equivalence class of ordered pair.
(Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | 2ecoptocl 6485* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | 3ecoptocl 6486* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 9-Aug-1995.)
|
|
|
Theorem | brecop 6487* |
Binary relation on a quotient set. Lemma for real number construction.
(Contributed by NM, 29-Jan-1996.)
|
|
|
Theorem | eroveu 6488* |
Lemma for eroprf 6490. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | erovlem 6489* |
Lemma for eroprf 6490. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | eroprf 6490* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | eroprf2 6491* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.)
|
|
|
Theorem | ecopoveq 6492* |
This is the first of several theorems about equivalence relations of
the kind used in construction of fractions and signed reals, involving
operations on equivalent classes of ordered pairs. This theorem
expresses the relation (specified by the hypothesis) in terms
of its operation . (Contributed by NM, 16-Aug-1995.)
|
|
|
Theorem | ecopovsym 6493* |
Assuming the operation is commutative, show that the relation
,
specified by the first hypothesis, is symmetric.
(Contributed by NM, 27-Aug-1995.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | ecopovtrn 6494* |
Assuming that operation is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
,
specified by the first hypothesis, is transitive.
(Contributed by NM, 11-Feb-1996.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | ecopover 6495* |
Assuming that operation is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
,
specified by the first hypothesis, is an equivalence
relation. (Contributed by NM, 16-Feb-1996.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ecopovsymg 6496* |
Assuming the operation is commutative, show that the relation
,
specified by the first hypothesis, is symmetric.
(Contributed by Jim Kingdon, 1-Sep-2019.)
|
|
|
Theorem | ecopovtrng 6497* |
Assuming that operation is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
,
specified by the first hypothesis, is transitive.
(Contributed by Jim Kingdon, 1-Sep-2019.)
|
|
|
Theorem | ecopoverg 6498* |
Assuming that operation is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
,
specified by the first hypothesis, is an equivalence
relation. (Contributed by Jim Kingdon, 1-Sep-2019.)
|
|
|
Theorem | th3qlem1 6499* |
Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60. The
third hypothesis is the compatibility assumption. (Contributed by NM,
3-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | th3qlem2 6500* |
Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60,
extended to operations on ordered pairs. The fourth hypothesis is the
compatibility assumption. (Contributed by NM, 4-Aug-1995.) (Revised by
Mario Carneiro, 12-Aug-2015.)
|
|