Theorem List for New Foundations Explorer - 4901-5000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | dfdm3 4901* |
Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring]
p. 24. (Contributed by set.mm contributors, 28-Dec-1996.)
|
|
|
Theorem | dfrn2 4902* |
Alternate definition of range. Definition 4 of [Suppes] p. 60.
(Contributed by set.mm contributors, 27-Dec-1996.)
|
|
|
Theorem | dfrn3 4903* |
Alternate definition of range. Definition 6.5(2) of [TakeutiZaring]
p. 24. (Contributed by set.mm contributors, 28-Dec-1996.)
|
|
|
Theorem | dfrn4 4904 |
Alternate definition of range. (Contributed by set.mm contributors,
5-Feb-2015.)
|
|
|
Theorem | dfdmf 4905* |
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 | dmss 4906 |
Subset theorem for domain. (Contributed by set.mm contributors,
11-Aug-1994.)
|
|
|
Theorem | dmeq 4907 |
Equality theorem for domain. (Contributed by set.mm contributors,
11-Aug-1994.)
|
|
|
Theorem | dmeqi 4908 |
Equality inference for domain. (Contributed by set.mm contributors,
4-Mar-2004.)
|
|
|
Theorem | dmeqd 4909 |
Equality deduction for domain. (Contributed by set.mm contributors,
4-Mar-2004.)
|
|
|
Theorem | opeldm 4910 |
Membership of first of an ordered pair in a domain. (Contributed by
set.mm contributors, 30-Jul-1995.)
|
|
|
Theorem | breldm 4911 |
Membership of first of a binary relation in a domain. (Contributed by
set.mm contributors, 8-Jan-2015.)
|
|
|
Theorem | dmun 4912 |
The domain of a union is the union of domains. Exercise 56(a) of
[Enderton] p. 65. (The proof was
shortened by Andrew Salmon,
27-Aug-2011.) (Contributed by set.mm contributors, 12-Aug-1994.)
(Revised by set.mm contributors, 27-Aug-2011.)
|
|
|
Theorem | dmin 4913 |
The domain of an intersection belong to the intersection of domains.
Theorem 6 of [Suppes] p. 60.
(Contributed by set.mm contributors,
15-Sep-2004.)
|
|
|
Theorem | dmuni 4914* |
The domain of a union. Part of Exercise 8 of [Enderton] p. 41.
(Contributed by set.mm contributors, 3-Feb-2004.)
|
|
|
Theorem | dmopab 4915* |
The domain of a class of ordered pairs. (Contributed by NM,
16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
|
|
Theorem | dmopabss 4916* |
Upper bound for the domain of a restricted class of ordered pairs.
(Contributed by set.mm contributors, 31-Jan-2004.)
|
|
|
Theorem | dmopab3 4917* |
The domain of a restricted class of ordered pairs. (Contributed by
set.mm contributors, 31-Jan-2004.)
|
|
|
Theorem | dm0 4918 |
The domain of the empty set is empty. Part of Theorem 3.8(v) of [Monk1]
p. 36. (The proof was shortened by Andrew Salmon, 27-Aug-2011.)
(Contributed by set.mm contributors, 4-Jul-1994.) (Revised by set.mm
contributors, 27-Aug-2011.)
|
|
|
Theorem | dmi 4919 |
The domain of the identity relation is the universe. (The proof was
shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm
contributors, 30-Apr-1998.) (Revised by set.mm contributors,
27-Aug-2011.)
|
|
|
Theorem | dmv 4920 |
The domain of the universe is the universe. (Contributed by set.mm
contributors, 8-Aug-2003.)
|
|
|
Theorem | dm0rn0 4921 |
An empty domain implies an empty range. (Contributed by set.mm
contributors, 21-May-1998.)
|
|
|
Theorem | dmeq0 4922 |
A class is empty iff its domain is empty. (Contributed by set.mm
contributors, 15-Sep-2004.) (Revised by Scott Fenton, 17-Apr-2021.)
|
|
|
Theorem | dmxp 4923 |
The domain of a cross product. Part of Theorem 3.13(x) of [Monk1]
p. 37. (The proof was shortened by Andrew Salmon, 27-Aug-2011.)
(Contributed by set.mm contributors, 28-Jul-1995.) (Revised by set.mm
contributors, 27-Aug-2011.)
|
|
|
Theorem | dmxpid 4924 |
The domain of a square cross product. (Contributed by set.mm
contributors, 28-Jul-1995.)
|
|
|
Theorem | dmxpin 4925 |
The domain of the intersection of two square cross products. Unlike
dmin 4913, equality holds. (Contributed by set.mm
contributors,
29-Jan-2008.)
|
|
|
Theorem | xpid11 4926 |
The cross product of a class with itself is one-to-one. (The proof was
shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm
contributors, 5-Nov-2006.) (Revised by set.mm contributors,
27-Aug-2011.)
|
|
|
Theorem | proj1eldm 4927 |
The first member of an ordered pair in a class belongs to the domain of
the class. (Contributed by set.mm contributors, 28-Jul-2004.) (Revised
by Scott Fenton, 18-Apr-2021.)
|
Proj1 |
|
Theorem | reseq1 4928 |
Equality theorem for restrictions. (Contributed by set.mm contributors,
7-Aug-1994.)
|
|
|
Theorem | reseq2 4929 |
Equality theorem for restrictions. (Contributed by set.mm contributors,
8-Aug-1994.)
|
|
|
Theorem | reseq1i 4930 |
Equality inference for restrictions. (Contributed by set.mm
contributors, 21-Oct-2014.)
|
|
|
Theorem | reseq2i 4931 |
Equality inference for restrictions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
|
|
Theorem | reseq12i 4932 |
Equality inference for restrictions. (Contributed by set.mm
contributors, 21-Oct-2014.)
|
|
|
Theorem | reseq1d 4933 |
Equality deduction for restrictions. (Contributed by set.mm
contributors, 21-Oct-2014.)
|
|
|
Theorem | reseq2d 4934 |
Equality deduction for restrictions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
|
|
Theorem | reseq12d 4935 |
Equality deduction for restrictions. (Contributed by set.mm
contributors, 21-Oct-2014.)
|
|
|
Theorem | nfres 4936 |
Bound-variable hypothesis builder for restriction. (Contributed by NM,
15-Sep-2003.) (Revised by David Abernethy, 19-Jun-2012.)
|
|
|
Theorem | imaeq1 4937 |
Equality theorem for image. (Contributed by set.mm contributors,
14-Aug-1994.)
|
|
|
Theorem | imaeq2 4938 |
Equality theorem for image. (Contributed by set.mm contributors,
14-Aug-1994.)
|
|
|
Theorem | imaeq1i 4939 |
Equality theorem for image. (Contributed by set.mm contributors,
21-Dec-2008.)
|
|
|
Theorem | imaeq2i 4940 |
Equality theorem for image. (Contributed by set.mm contributors,
21-Dec-2008.)
|
|
|
Theorem | imaeq1d 4941 |
Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
|
|
|
Theorem | imaeq2d 4942 |
Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
|
|
|
Theorem | imaeq12d 4943 |
Equality theorem for image. (Contributed by SF, 8-Jan-2018.)
|
|
|
Theorem | elimapw1 4944* |
Membership in an image under a unit power class. (Contributed by set.mm
contributors, 19-Feb-2015.)
|
1
|
|
Theorem | elimapw12 4945* |
Membership in an image under two unit power classes. (Contributed by
set.mm contributors, 18-Mar-2015.)
|
1 1 |
|
Theorem | elimapw13 4946* |
Membership in an image under three unit power classes. (Contributed by
set.mm contributors, 18-Mar-2015.)
|
1 1 1 |
|
Theorem | elima1c 4947* |
Membership in an image under cardinal one. (Contributed by set.mm
contributors, 6-Feb-2015.)
|
1c |
|
Theorem | elimapw11c 4948* |
Membership in an image under the unit power class of cardinal one.
(Contributed by set.mm contributors, 25-Feb-2015.)
|
1 1c |
|
Theorem | brres 4949 |
Binary relation on a restriction. (Contributed by set.mm contributors,
12-Dec-2006.)
|
|
|
Theorem | opelres 4950 |
Ordered pair membership in a restriction. Exercise 13 of [TakeutiZaring]
p. 25. (Contributed by set.mm contributors, 13-Nov-1995.)
|
|
|
Theorem | dfima3 4951 |
Alternate definition of image. (Contributed by set.mm contributors,
19-Apr-2004.) (Revised by set.mm contributors, 27-Aug-2011.)
|
|
|
Theorem | dfima4 4952* |
Alternate definition of image. Compare definition (d) of [Enderton]
p. 44. (The proof was shortened by Andrew Salmon, 27-Aug-2011.)
(Contributed by set.mm contributors, 14-Aug-1994.) (Revised by set.mm
contributors, 27-Aug-2011.)
|
|
|
Theorem | nfima 4953 |
Bound-variable hypothesis builder for image. (Contributed by NM,
30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | nfimad 4954 |
Deduction version of bound-variable hypothesis builder nfima 4953.
(Contributed by FL, 15-Dec-2006.) (Revised by Mario Carneiro,
15-Oct-2016.)
|
|
|
Theorem | csbima12g 4955 |
Move class substitution in and out of the image of a function.
(Contributed by FL, 15-Dec-2006.) (Proof shortened by Mario Carneiro,
4-Dec-2016.)
|
|
|
Theorem | rneq 4956 |
Equality theorem for range. (Contributed by set.mm contributors,
29-Dec-1996.)
|
|
|
Theorem | rneqi 4957 |
Equality inference for range. (Contributed by set.mm contributors,
4-Mar-2004.)
|
|
|
Theorem | rneqd 4958 |
Equality deduction for range. (Contributed by set.mm contributors,
4-Mar-2004.)
|
|
|
Theorem | rnss 4959 |
Subset theorem for range. (Contributed by set.mm contributors,
22-Mar-1998.)
|
|
|
Theorem | brelrn 4960 |
The second argument of a binary relation belongs to its range.
(Contributed by set.mm contributors, 29-Jun-2008.)
|
|
|
Theorem | opelrn 4961 |
Membership of second member of an ordered pair in a range. (Contributed
by set.mm contributors, 8-Jan-2015.)
|
|
|
Theorem | dfrnf 4962* |
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 | nfrn 4963 |
Bound-variable hypothesis builder for range. (Contributed by NM,
1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | nfdm 4964 |
Bound-variable hypothesis builder for domain. (Contributed by NM,
30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | dmiin 4965 |
Domain of an intersection. (Contributed by FL, 15-Oct-2012.)
|
|
|
Theorem | csbrng 4966 |
Distribute proper substitution through the range of a class.
(Contributed by Alan Sare, 10-Nov-2012.)
|
|
|
Theorem | rnopab 4967* |
The range of a class of ordered pairs. (Contributed by NM,
14-Aug-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
|
|
Theorem | rnopab2 4968* |
The range of a function expressed as a class abstraction. (Contributed
by set.mm contributors, 23-Mar-2006.)
|
|
|
Theorem | rn0 4969 |
The range of the empty set is empty. Part of Theorem 3.8(v) of [Monk1]
p. 36. (Contributed by set.mm contributors, 4-Jul-1994.)
|
|
|
Theorem | rneq0 4970 |
A relation is empty iff its range is empty. (Contributed by set.mm
contributors, 15-Sep-2004.) (Revised by Scott Fenton, 17-Apr-2021.)
|
|
|
Theorem | dmcoss 4971 |
Domain of a composition. Theorem 21 of [Suppes]
p. 63. (The proof was
shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm
contributors, 19-Mar-1998.) (Revised by set.mm contributors,
27-Aug-2011.)
|
|
|
Theorem | rncoss 4972 |
Range of a composition. (Contributed by set.mm contributors,
19-Mar-1998.)
|
|
|
Theorem | dmcosseq 4973 |
Domain of a composition. (The proof was shortened by Andrew Salmon,
27-Aug-2011.) (Contributed by set.mm contributors, 28-May-1998.)
(Revised by set.mm contributors, 27-Aug-2011.)
|
|
|
Theorem | dmcoeq 4974 |
Domain of a composition. (Contributed by set.mm contributors,
19-Mar-1998.)
|
|
|
Theorem | rncoeq 4975 |
Range of a composition. (Contributed by set.mm contributors,
19-Mar-1998.)
|
|
|
Theorem | csbresg 4976 |
Distribute proper substitution through the restriction of a class.
csbresg 4976 is derived from the virtual deduction proof
csbresgVD in set.mm.
(Contributed by Alan Sare, 10-Nov-2012.)
|
|
|
Theorem | res0 4977 |
A restriction to the empty set is empty. (Contributed by set.mm
contributors, 12-Nov-1994.)
|
|
|
Theorem | opres 4978 |
Ordered pair membership in a restriction when the first member belongs to
the restricting class. (The proof was shortened by Andrew Salmon,
27-Aug-2011.) (Contributed by set.mm contributors, 30-Apr-2004.)
(Revised by set.mm contributors, 27-Aug-2011.)
|
|
|
Theorem | resieq 4979 |
A restricted identity relation is equivalent to equality in its domain.
(Contributed by set.mm contributors, 30-Apr-2004.)
|
|
|
Theorem | resres 4980 |
The restriction of a restriction. (Contributed by set.mm contributors,
27-Mar-2008.)
|
|
|
Theorem | resundi 4981 |
Distributive law for restriction over union. Theorem 31 of [Suppes]
p. 65. (Contributed by set.mm contributors, 30-Sep-2002.)
|
|
|
Theorem | resundir 4982 |
Distributive law for restriction over union. (Contributed by set.mm
contributors, 23-Sep-2004.)
|
|
|
Theorem | resindi 4983 |
Class restriction distributes over intersection. (Contributed by FL,
6-Oct-2008.)
|
|
|
Theorem | resindir 4984 |
Class restriction distributes over intersection. (Contributed by set.mm
contributors, 18-Dec-2008.)
|
|
|
Theorem | inres 4985 |
Move intersection into class restriction. (Contributed by set.mm
contributors, 18-Dec-2008.)
|
|
|
Theorem | dmres 4986 |
The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25.
(Contributed by set.mm contributors, 1-Aug-1994.)
|
|
|
Theorem | ssdmres 4987 |
A domain restricted to a subclass equals the subclass. (Contributed by
set.mm contributors, 2-Mar-1997.) (Revised by set.mm contributors,
28-Aug-2004.)
|
|
|
Theorem | resss 4988 |
A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25.
(Contributed by set.mm contributors, 2-Aug-1994.)
|
|
|
Theorem | rescom 4989 |
Commutative law for restriction. (Contributed by set.mm contributors,
27-Mar-1998.)
|
|
|
Theorem | ssres 4990 |
Subclass theorem for restriction. (Contributed by set.mm contributors,
16-Aug-1994.)
|
|
|
Theorem | ssres2 4991 |
Subclass theorem for restriction. (The proof was shortened by Andrew
Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 22-Mar-1998.)
(Revised by set.mm contributors, 27-Aug-2011.)
|
|
|
Theorem | resabs1 4992 |
Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25.
(Contributed by set.mm contributors, 9-Aug-1994.)
|
|
|
Theorem | resabs2 4993 |
Absorption law for restriction. (Contributed by set.mm contributors,
27-Mar-1998.)
|
|
|
Theorem | residm 4994 |
Idempotent law for restriction. (Contributed by set.mm contributors,
27-Mar-1998.)
|
|
|
Theorem | elres 4995* |
Membership in a restriction. (Contributed by Scott Fenton,
17-Mar-2011.)
|
|
|
Theorem | elsnres 4996* |
Memebership in restriction to a singleton. (Contributed by Scott
Fenton, 17-Mar-2011.)
|
|
|
Theorem | ssreseq 4997 |
Simplification law for restriction. (Contributed by set.mm
contributors, 16-Aug-1994.) (Revised by set.mm contributors,
15-Mar-2004.) (Revised by Scott Fenton, 18-Apr-2021.)
|
|
|
Theorem | resdm 4998 |
A class restricted to its domain equals itself. (Contributed by set.mm
contributors, 12-Dec-2006.) (Revised by Scott Fenton, 18-Apr-2021.)
|
|
|
Theorem | resopab 4999* |
Restriction of a class abstraction of ordered pairs. (Contributed by
set.mm contributors, 5-Nov-2002.)
|
|
|
Theorem | iss 5000 |
A subclass of the identity function is the identity function restricted
to its domain. (The proof was shortened by Andrew Salmon, 27-Aug-2011.)
(Contributed by set.mm contributors, 13-Dec-2003.) (Revised by set.mm
contributors, 27-Aug-2011.)
|
|