Theorem List for Intuitionistic Logic Explorer - 4501-4600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | nfco 4501 |
Bound-variable hypothesis builder for function value. (Contributed by
NM, 1-Sep-1999.)
|
|
|
Theorem | brcog 4502* |
Ordered pair membership in a composition. (Contributed by NM,
24-Feb-2015.)
|
|
|
Theorem | opelco2g 4503* |
Ordered pair membership in a composition. (Contributed by NM,
27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.)
|
|
|
Theorem | brcogw 4504 |
Ordered pair membership in a composition. (Contributed by Thierry
Arnoux, 14-Jan-2018.)
|
|
|
Theorem | eqbrrdva 4505* |
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 4506* |
Binary relation on a composition. (Contributed by NM, 21-Sep-2004.)
(Revised by Mario Carneiro, 24-Feb-2015.)
|
|
|
Theorem | opelco 4507* |
Ordered pair membership in a composition. (Contributed by NM,
27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.)
|
|
|
Theorem | cnvss 4508 |
Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
|
|
|
Theorem | cnveq 4509 |
Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)
|
|
|
Theorem | cnveqi 4510 |
Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
|
|
|
Theorem | cnveqd 4511 |
Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)
|
|
|
Theorem | elcnv 4512* |
Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed
by NM, 24-Mar-1998.)
|
|
|
Theorem | elcnv2 4513* |
Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed
by NM, 11-Aug-2004.)
|
|
|
Theorem | nfcnv 4514 |
Bound-variable hypothesis builder for converse. (Contributed by NM,
31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | opelcnvg 4515 |
Ordered-pair membership in converse. (Contributed by NM, 13-May-1999.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | brcnvg 4516 |
The converse of a binary relation swaps arguments. Theorem 11 of [Suppes]
p. 61. (Contributed by NM, 10-Oct-2005.)
|
|
|
Theorem | opelcnv 4517 |
Ordered-pair membership in converse. (Contributed by NM,
13-Aug-1995.)
|
|
|
Theorem | brcnv 4518 |
The converse of a binary relation swaps arguments. Theorem 11 of
[Suppes] p. 61. (Contributed by NM,
13-Aug-1995.)
|
|
|
Theorem | csbcnvg 4519 |
Move class substitution in and out of the converse of a function.
(Contributed by Thierry Arnoux, 8-Feb-2017.)
|
|
|
Theorem | cnvco 4520 |
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 4521* |
The converse of a class union is the (indexed) union of the converses of
its members. (Contributed by NM, 11-Aug-2004.)
|
|
|
Theorem | dfdm3 4522* |
Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring]
p. 24. (Contributed by NM, 28-Dec-1996.)
|
|
|
Theorem | dfrn2 4523* |
Alternate definition of range. Definition 4 of [Suppes] p. 60.
(Contributed by NM, 27-Dec-1996.)
|
|
|
Theorem | dfrn3 4524* |
Alternate definition of range. Definition 6.5(2) of [TakeutiZaring]
p. 24. (Contributed by NM, 28-Dec-1996.)
|
|
|
Theorem | elrn2g 4525* |
Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
|
|
|
Theorem | elrng 4526* |
Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
|
|
|
Theorem | dfdm4 4527 |
Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
|
|
|
Theorem | dfdmf 4528* |
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 4529 |
Distribute proper substitution through the domain of a class.
(Contributed by Jim Kingdon, 8-Dec-2018.)
|
|
|
Theorem | eldmg 4530* |
Domain membership. Theorem 4 of [Suppes] p. 59.
(Contributed by Mario
Carneiro, 9-Jul-2014.)
|
|
|
Theorem | eldm2g 4531* |
Domain membership. Theorem 4 of [Suppes] p. 59.
(Contributed by NM,
27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | eldm 4532* |
Membership in a domain. Theorem 4 of [Suppes]
p. 59. (Contributed by
NM, 2-Apr-2004.)
|
|
|
Theorem | eldm2 4533* |
Membership in a domain. Theorem 4 of [Suppes]
p. 59. (Contributed by
NM, 1-Aug-1994.)
|
|
|
Theorem | dmss 4534 |
Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
|
|
|
Theorem | dmeq 4535 |
Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
|
|
|
Theorem | dmeqi 4536 |
Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
|
|
|
Theorem | dmeqd 4537 |
Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
|
|
|
Theorem | opeldm 4538 |
Membership of first of an ordered pair in a domain. (Contributed by NM,
30-Jul-1995.)
|
|
|
Theorem | breldm 4539 |
Membership of first of a binary relation in a domain. (Contributed by
NM, 30-Jul-1995.)
|
|
|
Theorem | opeldmg 4540 |
Membership of first of an ordered pair in a domain. (Contributed by Jim
Kingdon, 9-Jul-2019.)
|
|
|
Theorem | breldmg 4541 |
Membership of first of a binary relation in a domain. (Contributed by
NM, 21-Mar-2007.)
|
|
|
Theorem | dmun 4542 |
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 4543 |
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 4544 |
The domain of an indexed union. (Contributed by Mario Carneiro,
26-Apr-2016.)
|
|
|
Theorem | dmuni 4545* |
The domain of a union. Part of Exercise 8 of [Enderton] p. 41.
(Contributed by NM, 3-Feb-2004.)
|
|
|
Theorem | dmopab 4546* |
The domain of a class of ordered pairs. (Contributed by NM,
16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
|
|
Theorem | dmopabss 4547* |
Upper bound for the domain of a restricted class of ordered pairs.
(Contributed by NM, 31-Jan-2004.)
|
|
|
Theorem | dmopab3 4548* |
The domain of a restricted class of ordered pairs. (Contributed by NM,
31-Jan-2004.)
|
|
|
Theorem | dm0 4549 |
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 4550 |
The domain of the identity relation is the universe. (Contributed by
NM, 30-Apr-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | dmv 4551 |
The domain of the universe is the universe. (Contributed by NM,
8-Aug-2003.)
|
|
|
Theorem | dm0rn0 4552 |
An empty domain implies an empty range. (Contributed by NM,
21-May-1998.)
|
|
|
Theorem | reldm0 4553 |
A relation is empty iff its domain is empty. (Contributed by NM,
15-Sep-2004.)
|
|
|
Theorem | dmmrnm 4554* |
A domain is inhabited if and only if the range is inhabited.
(Contributed by Jim Kingdon, 15-Dec-2018.)
|
|
|
Theorem | dmxpm 4555* |
The domain of a cross product. Part of Theorem 3.13(x) of [Monk1]
p. 37. (Contributed by NM, 28-Jul-1995.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.)
|
|
|
Theorem | dmxpinm 4556* |
The domain of the intersection of two square cross products. Unlike
dmin 4543, equality holds. (Contributed by NM,
29-Jan-2008.)
|
|
|
Theorem | xpid11m 4557* |
The cross product of a class with itself is one-to-one. (Contributed by
Jim Kingdon, 8-Dec-2018.)
|
|
|
Theorem | dmcnvcnv 4558 |
The domain of the double converse of a class (which doesn't have to be a
relation as in dfrel2 4771). (Contributed by NM, 8-Apr-2007.)
|
|
|
Theorem | rncnvcnv 4559 |
The range of the double converse of a class. (Contributed by NM,
8-Apr-2007.)
|
|
|
Theorem | elreldm 4560 |
The first member of an ordered pair in a relation belongs to the domain
of the relation. (Contributed by NM, 28-Jul-2004.)
|
|
|
Theorem | rneq 4561 |
Equality theorem for range. (Contributed by NM, 29-Dec-1996.)
|
|
|
Theorem | rneqi 4562 |
Equality inference for range. (Contributed by NM, 4-Mar-2004.)
|
|
|
Theorem | rneqd 4563 |
Equality deduction for range. (Contributed by NM, 4-Mar-2004.)
|
|
|
Theorem | rnss 4564 |
Subset theorem for range. (Contributed by NM, 22-Mar-1998.)
|
|
|
Theorem | brelrng 4565 |
The second argument of a binary relation belongs to its range.
(Contributed by NM, 29-Jun-2008.)
|
|
|
Theorem | opelrng 4566 |
Membership of second member of an ordered pair in a range. (Contributed
by Jim Kingdon, 26-Jan-2019.)
|
|
|
Theorem | brelrn 4567 |
The second argument of a binary relation belongs to its range.
(Contributed by NM, 13-Aug-2004.)
|
|
|
Theorem | opelrn 4568 |
Membership of second member of an ordered pair in a range. (Contributed
by NM, 23-Feb-1997.)
|
|
|
Theorem | releldm 4569 |
The first argument of a binary relation belongs to its domain.
(Contributed by NM, 2-Jul-2008.)
|
|
|
Theorem | relelrn 4570 |
The second argument of a binary relation belongs to its range.
(Contributed by NM, 2-Jul-2008.)
|
|
|
Theorem | releldmb 4571* |
Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015.)
|
|
|
Theorem | relelrnb 4572* |
Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015.)
|
|
|
Theorem | releldmi 4573 |
The first argument of a binary relation belongs to its domain.
(Contributed by NM, 28-Apr-2015.)
|
|
|
Theorem | relelrni 4574 |
The second argument of a binary relation belongs to its range.
(Contributed by NM, 28-Apr-2015.)
|
|
|
Theorem | dfrnf 4575* |
Definition of range, using bound-variable hypotheses instead of distinct
variable conditions. (Contributed by NM, 14-Aug-1995.) (Revised by
Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | elrn2 4576* |
Membership in a range. (Contributed by NM, 10-Jul-1994.)
|
|
|
Theorem | elrn 4577* |
Membership in a range. (Contributed by NM, 2-Apr-2004.)
|
|
|
Theorem | nfdm 4578 |
Bound-variable hypothesis builder for domain. (Contributed by NM,
30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | nfrn 4579 |
Bound-variable hypothesis builder for range. (Contributed by NM,
1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | dmiin 4580 |
Domain of an intersection. (Contributed by FL, 15-Oct-2012.)
|
|
|
Theorem | rnopab 4581* |
The range of a class of ordered pairs. (Contributed by NM,
14-Aug-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
|
|
Theorem | rnmpt 4582* |
The range of a function in maps-to notation. (Contributed by Scott
Fenton, 21-Mar-2011.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | elrnmpt 4583* |
The range of a function in maps-to notation. (Contributed by Mario
Carneiro, 20-Feb-2015.)
|
|
|
Theorem | elrnmpt1s 4584* |
Elementhood in an image set. (Contributed by Mario Carneiro,
12-Sep-2015.)
|
|
|
Theorem | elrnmpt1 4585 |
Elementhood in an image set. (Contributed by Mario Carneiro,
31-Aug-2015.)
|
|
|
Theorem | elrnmptg 4586* |
Membership in the range of a function. (Contributed by NM,
27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | elrnmpti 4587* |
Membership in the range of a function. (Contributed by NM,
30-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | rn0 4588 |
The range of the empty set is empty. Part of Theorem 3.8(v) of [Monk1]
p. 36. (Contributed by NM, 4-Jul-1994.)
|
|
|
Theorem | dfiun3g 4589 |
Alternate definition of indexed union when is a set. (Contributed
by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | dfiin3g 4590 |
Alternate definition of indexed intersection when is a set.
(Contributed by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | dfiun3 4591 |
Alternate definition of indexed union when is a set. (Contributed
by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | dfiin3 4592 |
Alternate definition of indexed intersection when is a set.
(Contributed by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | riinint 4593* |
Express a relative indexed intersection as an intersection.
(Contributed by Stefan O'Rear, 22-Feb-2015.)
|
|
|
Theorem | relrn0 4594 |
A relation is empty iff its range is empty. (Contributed by NM,
15-Sep-2004.)
|
|
|
Theorem | dmrnssfld 4595 |
The domain and range of a class are included in its double union.
(Contributed by NM, 13-May-2008.)
|
|
|
Theorem | dmexg 4596 |
The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26.
(Contributed by NM, 7-Apr-1995.)
|
|
|
Theorem | rnexg 4597 |
The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26.
Similar to Lemma 3D of [Enderton] p. 41.
(Contributed by NM,
31-Mar-1995.)
|
|
|
Theorem | dmex 4598 |
The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring]
p. 26. (Contributed by NM, 7-Jul-2008.)
|
|
|
Theorem | rnex 4599 |
The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26.
Similar to Lemma 3D of [Enderton] p.
41. (Contributed by NM,
7-Jul-2008.)
|
|
|
Theorem | iprc 4600 |
The identity function is a proper class. This means, for example, that we
cannot use it as a member of the class of continuous functions unless it
is restricted to a set. (Contributed by NM, 1-Jan-2007.)
|
|