Home New Foundations ExplorerTheorem List (p. 50 of 64) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 4901-5000   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremdfdm3 4901* Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring] p. 24. (Contributed by set.mm contributors, 28-Dec-1996.)

Theoremdfrn2 4902* Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by set.mm contributors, 27-Dec-1996.)

Theoremdfrn3 4903* Alternate definition of range. Definition 6.5(2) of [TakeutiZaring] p. 24. (Contributed by set.mm contributors, 28-Dec-1996.)

Theoremdfrn4 4904 Alternate definition of range. (Contributed by set.mm contributors, 5-Feb-2015.)

Theoremdfdmf 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.)

Theoremdmss 4906 Subset theorem for domain. (Contributed by set.mm contributors, 11-Aug-1994.)

Theoremdmeq 4907 Equality theorem for domain. (Contributed by set.mm contributors, 11-Aug-1994.)

Theoremdmeqi 4908 Equality inference for domain. (Contributed by set.mm contributors, 4-Mar-2004.)

Theoremdmeqd 4909 Equality deduction for domain. (Contributed by set.mm contributors, 4-Mar-2004.)

Theoremopeldm 4910 Membership of first of an ordered pair in a domain. (Contributed by set.mm contributors, 30-Jul-1995.)

Theorembreldm 4911 Membership of first of a binary relation in a domain. (Contributed by set.mm contributors, 8-Jan-2015.)

Theoremdmun 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.)

Theoremdmin 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.)

Theoremdmuni 4914* The domain of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by set.mm contributors, 3-Feb-2004.)

Theoremdmopab 4915* The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)

Theoremdmopabss 4916* Upper bound for the domain of a restricted class of ordered pairs. (Contributed by set.mm contributors, 31-Jan-2004.)

Theoremdmopab3 4917* The domain of a restricted class of ordered pairs. (Contributed by set.mm contributors, 31-Jan-2004.)

Theoremdm0 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.)

Theoremdmi 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.)

Theoremdmv 4920 The domain of the universe is the universe. (Contributed by set.mm contributors, 8-Aug-2003.)

Theoremdm0rn0 4921 An empty domain implies an empty range. (Contributed by set.mm contributors, 21-May-1998.)

Theoremdmeq0 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.)

Theoremdmxp 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.)

Theoremdmxpid 4924 The domain of a square cross product. (Contributed by set.mm contributors, 28-Jul-1995.)

Theoremdmxpin 4925 The domain of the intersection of two square cross products. Unlike dmin 4913, equality holds. (Contributed by set.mm contributors, 29-Jan-2008.)

Theoremxpid11 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.)

Theoremproj1eldm 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

Theoremreseq1 4928 Equality theorem for restrictions. (Contributed by set.mm contributors, 7-Aug-1994.)

Theoremreseq2 4929 Equality theorem for restrictions. (Contributed by set.mm contributors, 8-Aug-1994.)

Theoremreseq1i 4930 Equality inference for restrictions. (Contributed by set.mm contributors, 21-Oct-2014.)

Theoremreseq2i 4931 Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)

Theoremreseq12i 4932 Equality inference for restrictions. (Contributed by set.mm contributors, 21-Oct-2014.)

Theoremreseq1d 4933 Equality deduction for restrictions. (Contributed by set.mm contributors, 21-Oct-2014.)

Theoremreseq2d 4934 Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)

Theoremreseq12d 4935 Equality deduction for restrictions. (Contributed by set.mm contributors, 21-Oct-2014.)

Theoremnfres 4936 Bound-variable hypothesis builder for restriction. (Contributed by NM, 15-Sep-2003.) (Revised by David Abernethy, 19-Jun-2012.)

Theoremimaeq1 4937 Equality theorem for image. (Contributed by set.mm contributors, 14-Aug-1994.)

Theoremimaeq2 4938 Equality theorem for image. (Contributed by set.mm contributors, 14-Aug-1994.)

Theoremimaeq1i 4939 Equality theorem for image. (Contributed by set.mm contributors, 21-Dec-2008.)

Theoremimaeq2i 4940 Equality theorem for image. (Contributed by set.mm contributors, 21-Dec-2008.)

Theoremimaeq1d 4941 Equality theorem for image. (Contributed by FL, 15-Dec-2006.)

Theoremimaeq2d 4942 Equality theorem for image. (Contributed by FL, 15-Dec-2006.)

Theoremimaeq12d 4943 Equality theorem for image. (Contributed by SF, 8-Jan-2018.)

Theoremelimapw1 4944* Membership in an image under a unit power class. (Contributed by set.mm contributors, 19-Feb-2015.)
1

Theoremelimapw12 4945* Membership in an image under two unit power classes. (Contributed by set.mm contributors, 18-Mar-2015.)
1 1

Theoremelimapw13 4946* Membership in an image under three unit power classes. (Contributed by set.mm contributors, 18-Mar-2015.)
1 1 1

Theoremelima1c 4947* Membership in an image under cardinal one. (Contributed by set.mm contributors, 6-Feb-2015.)
1c

Theoremelimapw11c 4948* Membership in an image under the unit power class of cardinal one. (Contributed by set.mm contributors, 25-Feb-2015.)
1 1c

Theorembrres 4949 Binary relation on a restriction. (Contributed by set.mm contributors, 12-Dec-2006.)

Theoremopelres 4950 Ordered pair membership in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by set.mm contributors, 13-Nov-1995.)

Theoremdfima3 4951 Alternate definition of image. (Contributed by set.mm contributors, 19-Apr-2004.) (Revised by set.mm contributors, 27-Aug-2011.)

Theoremdfima4 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.)

Theoremnfima 4953 Bound-variable hypothesis builder for image. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Theoremnfimad 4954 Deduction version of bound-variable hypothesis builder nfima 4953. (Contributed by FL, 15-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)

Theoremcsbima12g 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.)

Theoremrneq 4956 Equality theorem for range. (Contributed by set.mm contributors, 29-Dec-1996.)

Theoremrneqi 4957 Equality inference for range. (Contributed by set.mm contributors, 4-Mar-2004.)

Theoremrneqd 4958 Equality deduction for range. (Contributed by set.mm contributors, 4-Mar-2004.)

Theoremrnss 4959 Subset theorem for range. (Contributed by set.mm contributors, 22-Mar-1998.)

Theorembrelrn 4960 The second argument of a binary relation belongs to its range. (Contributed by set.mm contributors, 29-Jun-2008.)

Theoremopelrn 4961 Membership of second member of an ordered pair in a range. (Contributed by set.mm contributors, 8-Jan-2015.)

Theoremdfrnf 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.)

Theoremnfrn 4963 Bound-variable hypothesis builder for range. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.)

Theoremnfdm 4964 Bound-variable hypothesis builder for domain. (Contributed by NM, 30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)

Theoremdmiin 4965 Domain of an intersection. (Contributed by FL, 15-Oct-2012.)

Theoremcsbrng 4966 Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.)

Theoremrnopab 4967* The range of a class of ordered pairs. (Contributed by NM, 14-Aug-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)

Theoremrnopab2 4968* The range of a function expressed as a class abstraction. (Contributed by set.mm contributors, 23-Mar-2006.)

Theoremrn0 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.)

Theoremrneq0 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.)

Theoremdmcoss 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.)

Theoremrncoss 4972 Range of a composition. (Contributed by set.mm contributors, 19-Mar-1998.)

Theoremdmcosseq 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.)

Theoremdmcoeq 4974 Domain of a composition. (Contributed by set.mm contributors, 19-Mar-1998.)

Theoremrncoeq 4975 Range of a composition. (Contributed by set.mm contributors, 19-Mar-1998.)

Theoremcsbresg 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.)

Theoremres0 4977 A restriction to the empty set is empty. (Contributed by set.mm contributors, 12-Nov-1994.)

Theoremopres 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.)

Theoremresieq 4979 A restricted identity relation is equivalent to equality in its domain. (Contributed by set.mm contributors, 30-Apr-2004.)

Theoremresres 4980 The restriction of a restriction. (Contributed by set.mm contributors, 27-Mar-2008.)

Theoremresundi 4981 Distributive law for restriction over union. Theorem 31 of [Suppes] p. 65. (Contributed by set.mm contributors, 30-Sep-2002.)

Theoremresundir 4982 Distributive law for restriction over union. (Contributed by set.mm contributors, 23-Sep-2004.)

Theoremresindi 4983 Class restriction distributes over intersection. (Contributed by FL, 6-Oct-2008.)

Theoremresindir 4984 Class restriction distributes over intersection. (Contributed by set.mm contributors, 18-Dec-2008.)

Theoreminres 4985 Move intersection into class restriction. (Contributed by set.mm contributors, 18-Dec-2008.)

Theoremdmres 4986 The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25. (Contributed by set.mm contributors, 1-Aug-1994.)

Theoremssdmres 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.)

Theoremresss 4988 A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25. (Contributed by set.mm contributors, 2-Aug-1994.)

Theoremrescom 4989 Commutative law for restriction. (Contributed by set.mm contributors, 27-Mar-1998.)

Theoremssres 4990 Subclass theorem for restriction. (Contributed by set.mm contributors, 16-Aug-1994.)

Theoremssres2 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.)

Theoremresabs1 4992 Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25. (Contributed by set.mm contributors, 9-Aug-1994.)

Theoremresabs2 4993 Absorption law for restriction. (Contributed by set.mm contributors, 27-Mar-1998.)

Theoremresidm 4994 Idempotent law for restriction. (Contributed by set.mm contributors, 27-Mar-1998.)

Theoremelres 4995* Membership in a restriction. (Contributed by Scott Fenton, 17-Mar-2011.)

Theoremelsnres 4996* Memebership in restriction to a singleton. (Contributed by Scott Fenton, 17-Mar-2011.)

Theoremssreseq 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.)

Theoremresdm 4998 A class restricted to its domain equals itself. (Contributed by set.mm contributors, 12-Dec-2006.) (Revised by Scott Fenton, 18-Apr-2021.)

Theoremresopab 4999* Restriction of a class abstraction of ordered pairs. (Contributed by set.mm contributors, 5-Nov-2002.)

Theoremiss 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.)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6337
 Copyright terms: Public domain < Previous  Next >