Theorem List for Intuitionistic Logic Explorer - 4601-4700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | elrnmpt 4601* |
The range of a function in maps-to notation. (Contributed by Mario
Carneiro, 20-Feb-2015.)
|
|
|
Theorem | elrnmpt1s 4602* |
Elementhood in an image set. (Contributed by Mario Carneiro,
12-Sep-2015.)
|
|
|
Theorem | elrnmpt1 4603 |
Elementhood in an image set. (Contributed by Mario Carneiro,
31-Aug-2015.)
|
|
|
Theorem | elrnmptg 4604* |
Membership in the range of a function. (Contributed by NM,
27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | elrnmpti 4605* |
Membership in the range of a function. (Contributed by NM,
30-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | rn0 4606 |
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 4607 |
Alternate definition of indexed union when is a set. (Contributed
by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | dfiin3g 4608 |
Alternate definition of indexed intersection when is a set.
(Contributed by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | dfiun3 4609 |
Alternate definition of indexed union when is a set. (Contributed
by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | dfiin3 4610 |
Alternate definition of indexed intersection when is a set.
(Contributed by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | riinint 4611* |
Express a relative indexed intersection as an intersection.
(Contributed by Stefan O'Rear, 22-Feb-2015.)
|
|
|
Theorem | relrn0 4612 |
A relation is empty iff its range is empty. (Contributed by NM,
15-Sep-2004.)
|
|
|
Theorem | dmrnssfld 4613 |
The domain and range of a class are included in its double union.
(Contributed by NM, 13-May-2008.)
|
|
|
Theorem | dmexg 4614 |
The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26.
(Contributed by NM, 7-Apr-1995.)
|
|
|
Theorem | rnexg 4615 |
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 4616 |
The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring]
p. 26. (Contributed by NM, 7-Jul-2008.)
|
|
|
Theorem | rnex 4617 |
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 4618 |
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.)
|
|
|
Theorem | dmcoss 4619 |
Domain of a composition. Theorem 21 of [Suppes]
p. 63. (Contributed by
NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | rncoss 4620 |
Range of a composition. (Contributed by NM, 19-Mar-1998.)
|
|
|
Theorem | dmcosseq 4621 |
Domain of a composition. (Contributed by NM, 28-May-1998.) (Proof
shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | dmcoeq 4622 |
Domain of a composition. (Contributed by NM, 19-Mar-1998.)
|
|
|
Theorem | rncoeq 4623 |
Range of a composition. (Contributed by NM, 19-Mar-1998.)
|
|
|
Theorem | reseq1 4624 |
Equality theorem for restrictions. (Contributed by NM, 7-Aug-1994.)
|
|
|
Theorem | reseq2 4625 |
Equality theorem for restrictions. (Contributed by NM, 8-Aug-1994.)
|
|
|
Theorem | reseq1i 4626 |
Equality inference for restrictions. (Contributed by NM,
21-Oct-2014.)
|
|
|
Theorem | reseq2i 4627 |
Equality inference for restrictions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
|
|
Theorem | reseq12i 4628 |
Equality inference for restrictions. (Contributed by NM,
21-Oct-2014.)
|
|
|
Theorem | reseq1d 4629 |
Equality deduction for restrictions. (Contributed by NM,
21-Oct-2014.)
|
|
|
Theorem | reseq2d 4630 |
Equality deduction for restrictions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
|
|
Theorem | reseq12d 4631 |
Equality deduction for restrictions. (Contributed by NM,
21-Oct-2014.)
|
|
|
Theorem | nfres 4632 |
Bound-variable hypothesis builder for restriction. (Contributed by NM,
15-Sep-2003.) (Revised by David Abernethy, 19-Jun-2012.)
|
|
|
Theorem | csbresg 4633 |
Distribute proper substitution through the restriction of a class.
(Contributed by Alan Sare, 10-Nov-2012.)
|
|
|
Theorem | res0 4634 |
A restriction to the empty set is empty. (Contributed by NM,
12-Nov-1994.)
|
|
|
Theorem | opelres 4635 |
Ordered pair membership in a restriction. Exercise 13 of
[TakeutiZaring] p. 25.
(Contributed by NM, 13-Nov-1995.)
|
|
|
Theorem | brres 4636 |
Binary relation on a restriction. (Contributed by NM, 12-Dec-2006.)
|
|
|
Theorem | opelresg 4637 |
Ordered pair membership in a restriction. Exercise 13 of
[TakeutiZaring] p. 25.
(Contributed by NM, 14-Oct-2005.)
|
|
|
Theorem | brresg 4638 |
Binary relation on a restriction. (Contributed by Mario Carneiro,
4-Nov-2015.)
|
|
|
Theorem | opres 4639 |
Ordered pair membership in a restriction when the first member belongs
to the restricting class. (Contributed by NM, 30-Apr-2004.) (Proof
shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | resieq 4640 |
A restricted identity relation is equivalent to equality in its domain.
(Contributed by NM, 30-Apr-2004.)
|
|
|
Theorem | opelresi 4641 |
belongs to a restriction of the identity class iff
belongs to the restricting class. (Contributed by FL, 27-Oct-2008.)
(Revised by NM, 30-Mar-2016.)
|
|
|
Theorem | resres 4642 |
The restriction of a restriction. (Contributed by NM, 27-Mar-2008.)
|
|
|
Theorem | resundi 4643 |
Distributive law for restriction over union. Theorem 31 of [Suppes]
p. 65. (Contributed by NM, 30-Sep-2002.)
|
|
|
Theorem | resundir 4644 |
Distributive law for restriction over union. (Contributed by NM,
23-Sep-2004.)
|
|
|
Theorem | resindi 4645 |
Class restriction distributes over intersection. (Contributed by FL,
6-Oct-2008.)
|
|
|
Theorem | resindir 4646 |
Class restriction distributes over intersection. (Contributed by NM,
18-Dec-2008.)
|
|
|
Theorem | inres 4647 |
Move intersection into class restriction. (Contributed by NM,
18-Dec-2008.)
|
|
|
Theorem | resiun1 4648* |
Distribution of restriction over indexed union. (Contributed by Mario
Carneiro, 29-May-2015.)
|
|
|
Theorem | resiun2 4649* |
Distribution of restriction over indexed union. (Contributed by Mario
Carneiro, 29-May-2015.)
|
|
|
Theorem | dmres 4650 |
The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25.
(Contributed by NM, 1-Aug-1994.)
|
|
|
Theorem | ssdmres 4651 |
A domain restricted to a subclass equals the subclass. (Contributed by
NM, 2-Mar-1997.)
|
|
|
Theorem | dmresexg 4652 |
The domain of a restriction to a set exists. (Contributed by NM,
7-Apr-1995.)
|
|
|
Theorem | resss 4653 |
A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25.
(Contributed by NM, 2-Aug-1994.)
|
|
|
Theorem | rescom 4654 |
Commutative law for restriction. (Contributed by NM, 27-Mar-1998.)
|
|
|
Theorem | ssres 4655 |
Subclass theorem for restriction. (Contributed by NM, 16-Aug-1994.)
|
|
|
Theorem | ssres2 4656 |
Subclass theorem for restriction. (Contributed by NM, 22-Mar-1998.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | relres 4657 |
A restriction is a relation. Exercise 12 of [TakeutiZaring] p. 25.
(Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon,
27-Aug-2011.)
|
|
|
Theorem | resabs1 4658 |
Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25.
(Contributed by NM, 9-Aug-1994.)
|
|
|
Theorem | resabs2 4659 |
Absorption law for restriction. (Contributed by NM, 27-Mar-1998.)
|
|
|
Theorem | residm 4660 |
Idempotent law for restriction. (Contributed by NM, 27-Mar-1998.)
|
|
|
Theorem | resima 4661 |
A restriction to an image. (Contributed by NM, 29-Sep-2004.)
|
|
|
Theorem | resima2 4662 |
Image under a restricted class. (Contributed by FL, 31-Aug-2009.)
|
|
|
Theorem | xpssres 4663 |
Restriction of a constant function (or other cross product). (Contributed
by Stefan O'Rear, 24-Jan-2015.)
|
|
|
Theorem | elres 4664* |
Membership in a restriction. (Contributed by Scott Fenton,
17-Mar-2011.)
|
|
|
Theorem | elsnres 4665* |
Memebership in restriction to a singleton. (Contributed by Scott
Fenton, 17-Mar-2011.)
|
|
|
Theorem | relssres 4666 |
Simplification law for restriction. (Contributed by NM,
16-Aug-1994.)
|
|
|
Theorem | resdm 4667 |
A relation restricted to its domain equals itself. (Contributed by NM,
12-Dec-2006.)
|
|
|
Theorem | resexg 4668 |
The restriction of a set is a set. (Contributed by NM, 28-Mar-1998.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | resex 4669 |
The restriction of a set is a set. (Contributed by Jeff Madsen,
19-Jun-2011.)
|
|
|
Theorem | resindm 4670 |
When restricting a relation, intersecting with the domain of the relation
has no effect. (Contributed by FL, 6-Oct-2008.)
|
|
|
Theorem | resdmdfsn 4671 |
Restricting a relation to its domain without a set is the same as
restricting the relation to the universe without this set. (Contributed
by AV, 2-Dec-2018.)
|
|
|
Theorem | resopab 4672* |
Restriction of a class abstraction of ordered pairs. (Contributed by
NM, 5-Nov-2002.)
|
|
|
Theorem | resiexg 4673 |
The existence of a restricted identity function, proved without using
the Axiom of Replacement. (Contributed by NM, 13-Jan-2007.)
|
|
|
Theorem | iss 4674 |
A subclass of the identity function is the identity function restricted
to its domain. (Contributed by NM, 13-Dec-2003.) (Proof shortened by
Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | resopab2 4675* |
Restriction of a class abstraction of ordered pairs. (Contributed by
NM, 24-Aug-2007.)
|
|
|
Theorem | resmpt 4676* |
Restriction of the mapping operation. (Contributed by Mario Carneiro,
15-Jul-2013.)
|
|
|
Theorem | resmpt3 4677* |
Unconditional restriction of the mapping operation. (Contributed by
Stefan O'Rear, 24-Jan-2015.) (Proof shortened by Mario Carneiro,
22-Mar-2015.)
|
|
|
Theorem | dfres2 4678* |
Alternate definition of the restriction operation. (Contributed by
Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | opabresid 4679* |
The restricted identity expressed with the class builder. (Contributed
by FL, 25-Apr-2012.)
|
|
|
Theorem | mptresid 4680* |
The restricted identity expressed with the "maps to" notation.
(Contributed by FL, 25-Apr-2012.)
|
|
|
Theorem | dmresi 4681 |
The domain of a restricted identity function. (Contributed by NM,
27-Aug-2004.)
|
|
|
Theorem | resid 4682 |
Any relation restricted to the universe is itself. (Contributed by NM,
16-Mar-2004.)
|
|
|
Theorem | imaeq1 4683 |
Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
|
|
|
Theorem | imaeq2 4684 |
Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
|
|
|
Theorem | imaeq1i 4685 |
Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
|
|
|
Theorem | imaeq2i 4686 |
Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
|
|
|
Theorem | imaeq1d 4687 |
Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
|
|
|
Theorem | imaeq2d 4688 |
Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
|
|
|
Theorem | imaeq12d 4689 |
Equality theorem for image. (Contributed by Mario Carneiro,
4-Dec-2016.)
|
|
|
Theorem | dfima2 4690* |
Alternate definition of image. Compare definition (d) of [Enderton]
p. 44. (Contributed by NM, 19-Apr-2004.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.)
|
|
|
Theorem | dfima3 4691* |
Alternate definition of image. Compare definition (d) of [Enderton]
p. 44. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.)
|
|
|
Theorem | elimag 4692* |
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 20-Jan-2007.)
|
|
|
Theorem | elima 4693* |
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 19-Apr-2004.)
|
|
|
Theorem | elima2 4694* |
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 11-Aug-2004.)
|
|
|
Theorem | elima3 4695* |
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 14-Aug-1994.)
|
|
|
Theorem | nfima 4696 |
Bound-variable hypothesis builder for image. (Contributed by NM,
30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | nfimad 4697 |
Deduction version of bound-variable hypothesis builder nfima 4696.
(Contributed by FL, 15-Dec-2006.) (Revised by Mario Carneiro,
15-Oct-2016.)
|
|
|
Theorem | imadmrn 4698 |
The image of the domain of a class is the range of the class.
(Contributed by NM, 14-Aug-1994.)
|
|
|
Theorem | imassrn 4699 |
The image of a class is a subset of its range. Theorem 3.16(xi) of
[Monk1] p. 39. (Contributed by NM,
31-Mar-1995.)
|
|
|
Theorem | imaexg 4700 |
The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed
by NM, 24-Jul-1995.)
|
|