HomeHome New Foundations Explorer
Theorem 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.)
 F/_   &     F/_   =>   
 
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.)
 F/_   &     F/_   =>     F/_
 
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.)
 F/_   &     F/_   =>     F/_
 
Theoremnfimad 4954 Deduction version of bound-variable hypothesis builder nfima 4953. (Contributed by FL, 15-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
 F/_   &     F/_   =>     F/_
 
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.)
 F/_   &     F/_   =>   
 
Theoremnfrn 4963 Bound-variable hypothesis builder for range. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.)
 F/_   =>     F/_
 
Theoremnfdm 4964 Bound-variable hypothesis builder for domain. (Contributed by NM, 30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
 F/_   =>     F/_
 
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.)
    < Previous  Next >

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-6338
  Copyright terms: Public domain < Previous  Next >