Theorem List for Intuitionistic Logic Explorer - 4701-4800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | sqxpexg 4701 |
The Cartesian square of a set is a set. (Contributed by AV,
13-Jan-2020.)
|
|
|
Theorem | relun 4702 |
The union of two relations is a relation. Compare Exercise 5 of
[TakeutiZaring] p. 25. (Contributed
by NM, 12-Aug-1994.)
|
|
|
Theorem | relin1 4703 |
The intersection with a relation is a relation. (Contributed by NM,
16-Aug-1994.)
|
|
|
Theorem | relin2 4704 |
The intersection with a relation is a relation. (Contributed by NM,
17-Jan-2006.)
|
|
|
Theorem | reldif 4705 |
A difference cutting down a relation is a relation. (Contributed by NM,
31-Mar-1998.)
|
|
|
Theorem | reliun 4706 |
An indexed union is a relation iff each member of its indexed family is
a relation. (Contributed by NM, 19-Dec-2008.)
|
|
|
Theorem | reliin 4707 |
An indexed intersection is a relation if at least one of the member of the
indexed family is a relation. (Contributed by NM, 8-Mar-2014.)
|
|
|
Theorem | reluni 4708* |
The union of a class is a relation iff any member is a relation.
Exercise 6 of [TakeutiZaring] p.
25 and its converse. (Contributed by
NM, 13-Aug-2004.)
|
|
|
Theorem | relint 4709* |
The intersection of a class is a relation if at least one member is a
relation. (Contributed by NM, 8-Mar-2014.)
|
|
|
Theorem | rel0 4710 |
The empty set is a relation. (Contributed by NM, 26-Apr-1998.)
|
|
|
Theorem | relopabi 4711 |
A class of ordered pairs is a relation. (Contributed by Mario Carneiro,
21-Dec-2013.)
|
|
|
Theorem | relopab 4712 |
A class of ordered pairs is a relation. (Contributed by NM, 8-Mar-1995.)
(Unnecessary distinct variable restrictions were removed by Alan Sare,
9-Jul-2013.) (Proof shortened by Mario Carneiro, 21-Dec-2013.)
|
|
|
Theorem | mptrel 4713 |
The maps-to notation always describes a relationship. (Contributed by
Scott Fenton, 16-Apr-2012.)
|
|
|
Theorem | reli 4714 |
The identity relation is a relation. Part of Exercise 4.12(p) of
[Mendelson] p. 235. (Contributed by
NM, 26-Apr-1998.) (Revised by
Mario Carneiro, 21-Dec-2013.)
|
|
|
Theorem | rele 4715 |
The membership relation is a relation. (Contributed by NM,
26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)
|
|
|
Theorem | opabid2 4716* |
A relation expressed as an ordered pair abstraction. (Contributed by
NM, 11-Dec-2006.)
|
|
|
Theorem | inopab 4717* |
Intersection of two ordered pair class abstractions. (Contributed by
NM, 30-Sep-2002.)
|
|
|
Theorem | difopab 4718* |
The difference of two ordered-pair abstractions. (Contributed by Stefan
O'Rear, 17-Jan-2015.)
|
|
|
Theorem | inxp 4719 |
The intersection of two cross products. Exercise 9 of [TakeutiZaring]
p. 25. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.)
|
|
|
Theorem | xpindi 4720 |
Distributive law for cross product over intersection. Theorem 102 of
[Suppes] p. 52. (Contributed by NM,
26-Sep-2004.)
|
|
|
Theorem | xpindir 4721 |
Distributive law for cross product over intersection. Similar to
Theorem 102 of [Suppes] p. 52.
(Contributed by NM, 26-Sep-2004.)
|
|
|
Theorem | xpiindim 4722* |
Distributive law for cross product over indexed intersection.
(Contributed by Jim Kingdon, 7-Dec-2018.)
|
|
|
Theorem | xpriindim 4723* |
Distributive law for cross product over relativized indexed
intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
|
|
|
Theorem | eliunxp 4724* |
Membership in a union of cross products. Analogue of elxp 4602
for
nonconstant . (Contributed by Mario Carneiro,
29-Dec-2014.)
|
|
|
Theorem | opeliunxp2 4725* |
Membership in a union of cross products. (Contributed by Mario
Carneiro, 14-Feb-2015.)
|
|
|
Theorem | raliunxp 4726* |
Write a double restricted quantification as one universal quantifier.
In this version of ralxp 4728, is not assumed to be constant.
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
|
|
Theorem | rexiunxp 4727* |
Write a double restricted quantification as one universal quantifier.
In this version of rexxp 4729, is not assumed to be constant.
(Contributed by Mario Carneiro, 14-Feb-2015.)
|
|
|
Theorem | ralxp 4728* |
Universal quantification restricted to a cross product is equivalent to
a double restricted quantification. The hypothesis specifies an
implicit substitution. (Contributed by NM, 7-Feb-2004.) (Revised by
Mario Carneiro, 29-Dec-2014.)
|
|
|
Theorem | rexxp 4729* |
Existential quantification restricted to a cross product is equivalent
to a double restricted quantification. (Contributed by NM,
11-Nov-1995.) (Revised by Mario Carneiro, 14-Feb-2015.)
|
|
|
Theorem | djussxp 4730* |
Disjoint union is a subset of a cross product. (Contributed by Stefan
O'Rear, 21-Nov-2014.)
|
|
|
Theorem | ralxpf 4731* |
Version of ralxp 4728 with bound-variable hypotheses. (Contributed
by NM,
18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | rexxpf 4732* |
Version of rexxp 4729 with bound-variable hypotheses. (Contributed
by NM,
19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | iunxpf 4733* |
Indexed union on a cross product is equals a double indexed union. The
hypothesis specifies an implicit substitution. (Contributed by NM,
19-Dec-2008.)
|
|
|
Theorem | opabbi2dv 4734* |
Deduce equality of a relation and an ordered-pair class builder.
Compare abbi2dv 2276. (Contributed by NM, 24-Feb-2014.)
|
|
|
Theorem | relop 4735* |
A necessary and sufficient condition for a Kuratowski ordered pair to be
a relation. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this
detail.)
|
|
|
Theorem | ideqg 4736 |
For sets, the identity relation is the same as equality. (Contributed
by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon,
27-Aug-2011.)
|
|
|
Theorem | ideq 4737 |
For sets, the identity relation is the same as equality. (Contributed
by NM, 13-Aug-1995.)
|
|
|
Theorem | ididg 4738 |
A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof
shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | issetid 4739 |
Two ways of expressing set existence. (Contributed by NM, 16-Feb-2008.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario
Carneiro, 26-Apr-2015.)
|
|
|
Theorem | coss1 4740 |
Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
|
|
|
Theorem | coss2 4741 |
Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
|
|
|
Theorem | coeq1 4742 |
Equality theorem for composition of two classes. (Contributed by NM,
3-Jan-1997.)
|
|
|
Theorem | coeq2 4743 |
Equality theorem for composition of two classes. (Contributed by NM,
3-Jan-1997.)
|
|
|
Theorem | coeq1i 4744 |
Equality inference for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
|
|
Theorem | coeq2i 4745 |
Equality inference for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
|
|
Theorem | coeq1d 4746 |
Equality deduction for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
|
|
Theorem | coeq2d 4747 |
Equality deduction for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
|
|
Theorem | coeq12i 4748 |
Equality inference for composition of two classes. (Contributed by FL,
7-Jun-2012.)
|
|
|
Theorem | coeq12d 4749 |
Equality deduction for composition of two classes. (Contributed by FL,
7-Jun-2012.)
|
|
|
Theorem | nfco 4750 |
Bound-variable hypothesis builder for function value. (Contributed by
NM, 1-Sep-1999.)
|
|
|
Theorem | elco 4751* |
Elements of a composed relation. (Contributed by BJ, 10-Jul-2022.)
|
|
|
Theorem | brcog 4752* |
Ordered pair membership in a composition. (Contributed by NM,
24-Feb-2015.)
|
|
|
Theorem | opelco2g 4753* |
Ordered pair membership in a composition. (Contributed by NM,
27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.)
|
|
|
Theorem | brcogw 4754 |
Ordered pair membership in a composition. (Contributed by Thierry
Arnoux, 14-Jan-2018.)
|
|
|
Theorem | eqbrrdva 4755* |
Deduction from extensionality principle for relations, given an
equivalence only on the relation's domain and range. (Contributed by
Thierry Arnoux, 28-Nov-2017.)
|
|
|
Theorem | brco 4756* |
Binary relation on a composition. (Contributed by NM, 21-Sep-2004.)
(Revised by Mario Carneiro, 24-Feb-2015.)
|
|
|
Theorem | opelco 4757* |
Ordered pair membership in a composition. (Contributed by NM,
27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.)
|
|
|
Theorem | cnvss 4758 |
Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
|
|
|
Theorem | cnveq 4759 |
Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)
|
|
|
Theorem | cnveqi 4760 |
Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
|
|
|
Theorem | cnveqd 4761 |
Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)
|
|
|
Theorem | elcnv 4762* |
Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed
by NM, 24-Mar-1998.)
|
|
|
Theorem | elcnv2 4763* |
Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed
by NM, 11-Aug-2004.)
|
|
|
Theorem | nfcnv 4764 |
Bound-variable hypothesis builder for converse. (Contributed by NM,
31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | opelcnvg 4765 |
Ordered-pair membership in converse. (Contributed by NM, 13-May-1999.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | brcnvg 4766 |
The converse of a binary relation swaps arguments. Theorem 11 of [Suppes]
p. 61. (Contributed by NM, 10-Oct-2005.)
|
|
|
Theorem | opelcnv 4767 |
Ordered-pair membership in converse. (Contributed by NM,
13-Aug-1995.)
|
|
|
Theorem | brcnv 4768 |
The converse of a binary relation swaps arguments. Theorem 11 of
[Suppes] p. 61. (Contributed by NM,
13-Aug-1995.)
|
|
|
Theorem | csbcnvg 4769 |
Move class substitution in and out of the converse of a function.
(Contributed by Thierry Arnoux, 8-Feb-2017.)
|
|
|
Theorem | cnvco 4770 |
Distributive law of converse over class composition. Theorem 26 of
[Suppes] p. 64. (Contributed by NM,
19-Mar-1998.) (Proof shortened by
Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | cnvuni 4771* |
The converse of a class union is the (indexed) union of the converses of
its members. (Contributed by NM, 11-Aug-2004.)
|
|
|
Theorem | dfdm3 4772* |
Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring]
p. 24. (Contributed by NM, 28-Dec-1996.)
|
|
|
Theorem | dfrn2 4773* |
Alternate definition of range. Definition 4 of [Suppes] p. 60.
(Contributed by NM, 27-Dec-1996.)
|
|
|
Theorem | dfrn3 4774* |
Alternate definition of range. Definition 6.5(2) of [TakeutiZaring]
p. 24. (Contributed by NM, 28-Dec-1996.)
|
|
|
Theorem | elrn2g 4775* |
Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
|
|
|
Theorem | elrng 4776* |
Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
|
|
|
Theorem | dfdm4 4777 |
Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
|
|
|
Theorem | dfdmf 4778* |
Definition of domain, using bound-variable hypotheses instead of
distinct variable conditions. (Contributed by NM, 8-Mar-1995.)
(Revised by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | csbdmg 4779 |
Distribute proper substitution through the domain of a class.
(Contributed by Jim Kingdon, 8-Dec-2018.)
|
|
|
Theorem | eldmg 4780* |
Domain membership. Theorem 4 of [Suppes] p. 59.
(Contributed by Mario
Carneiro, 9-Jul-2014.)
|
|
|
Theorem | eldm2g 4781* |
Domain membership. Theorem 4 of [Suppes] p. 59.
(Contributed by NM,
27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | eldm 4782* |
Membership in a domain. Theorem 4 of [Suppes]
p. 59. (Contributed by
NM, 2-Apr-2004.)
|
|
|
Theorem | eldm2 4783* |
Membership in a domain. Theorem 4 of [Suppes]
p. 59. (Contributed by
NM, 1-Aug-1994.)
|
|
|
Theorem | dmss 4784 |
Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
|
|
|
Theorem | dmeq 4785 |
Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
|
|
|
Theorem | dmeqi 4786 |
Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
|
|
|
Theorem | dmeqd 4787 |
Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
|
|
|
Theorem | opeldm 4788 |
Membership of first of an ordered pair in a domain. (Contributed by NM,
30-Jul-1995.)
|
|
|
Theorem | breldm 4789 |
Membership of first of a binary relation in a domain. (Contributed by
NM, 30-Jul-1995.)
|
|
|
Theorem | opeldmg 4790 |
Membership of first of an ordered pair in a domain. (Contributed by Jim
Kingdon, 9-Jul-2019.)
|
|
|
Theorem | breldmg 4791 |
Membership of first of a binary relation in a domain. (Contributed by
NM, 21-Mar-2007.)
|
|
|
Theorem | dmun 4792 |
The domain of a union is the union of domains. Exercise 56(a) of
[Enderton] p. 65. (Contributed by NM,
12-Aug-1994.) (Proof shortened
by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | dmin 4793 |
The domain of an intersection belong to the intersection of domains.
Theorem 6 of [Suppes] p. 60.
(Contributed by NM, 15-Sep-2004.)
|
|
|
Theorem | dmiun 4794 |
The domain of an indexed union. (Contributed by Mario Carneiro,
26-Apr-2016.)
|
|
|
Theorem | dmuni 4795* |
The domain of a union. Part of Exercise 8 of [Enderton] p. 41.
(Contributed by NM, 3-Feb-2004.)
|
|
|
Theorem | dmopab 4796* |
The domain of a class of ordered pairs. (Contributed by NM,
16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
|
|
Theorem | dmopabss 4797* |
Upper bound for the domain of a restricted class of ordered pairs.
(Contributed by NM, 31-Jan-2004.)
|
|
|
Theorem | dmopab3 4798* |
The domain of a restricted class of ordered pairs. (Contributed by NM,
31-Jan-2004.)
|
|
|
Theorem | dm0 4799 |
The domain of the empty set is empty. Part of Theorem 3.8(v) of [Monk1]
p. 36. (Contributed by NM, 4-Jul-1994.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.)
|
|
|
Theorem | dmi 4800 |
The domain of the identity relation is the universe. (Contributed by
NM, 30-Apr-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|