HomeHome New Foundations Explorer
Theorem List (p. 50 of 64)
< Previous  Next >
Bad symbols? Try the
GIF 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.)
dom A = {x yx, y A}
 
Theoremdfrn2 4902* Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by set.mm contributors, 27-Dec-1996.)
ran A = {y x xAy}
 
Theoremdfrn3 4903* Alternate definition of range. Definition 6.5(2) of [TakeutiZaring] p. 24. (Contributed by set.mm contributors, 28-Dec-1996.)
ran A = {y xx, y A}
 
Theoremdfrn4 4904 Alternate definition of range. (Contributed by set.mm contributors, 5-Feb-2015.)
ran A = dom A
 
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.)
xA    &   yA       dom A = {x y xAy}
 
Theoremdmss 4906 Subset theorem for domain. (Contributed by set.mm contributors, 11-Aug-1994.)
(A B → dom A dom B)
 
Theoremdmeq 4907 Equality theorem for domain. (Contributed by set.mm contributors, 11-Aug-1994.)
(A = B → dom A = dom B)
 
Theoremdmeqi 4908 Equality inference for domain. (Contributed by set.mm contributors, 4-Mar-2004.)
A = B       dom A = dom B
 
Theoremdmeqd 4909 Equality deduction for domain. (Contributed by set.mm contributors, 4-Mar-2004.)
(φA = B)       (φ → dom A = dom B)
 
Theoremopeldm 4910 Membership of first of an ordered pair in a domain. (Contributed by set.mm contributors, 30-Jul-1995.)
(A, B CA dom C)
 
Theorembreldm 4911 Membership of first of a binary relation in a domain. (Contributed by set.mm contributors, 8-Jan-2015.)
(ARBA dom R)
 
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.)
dom (AB) = (dom A ∪ dom B)
 
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.)
dom (AB) (dom A ∩ dom B)
 
Theoremdmuni 4914* The domain of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by set.mm contributors, 3-Feb-2004.)
dom A = x A dom x
 
Theoremdmopab 4915* The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
dom {x, y φ} = {x yφ}
 
Theoremdmopabss 4916* Upper bound for the domain of a restricted class of ordered pairs. (Contributed by set.mm contributors, 31-Jan-2004.)
dom {x, y (x A φ)} A
 
Theoremdmopab3 4917* The domain of a restricted class of ordered pairs. (Contributed by set.mm contributors, 31-Jan-2004.)
(x A yφ ↔ dom {x, y (x A φ)} = A)
 
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.)
dom =
 
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.)
dom I = V
 
Theoremdmv 4920 The domain of the universe is the universe. (Contributed by set.mm contributors, 8-Aug-2003.)
dom V = V
 
Theoremdm0rn0 4921 An empty domain implies an empty range. (Contributed by set.mm contributors, 21-May-1998.)
(dom A = ↔ ran A = )
 
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.)
(A = ↔ dom A = )
 
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.)
(B → dom (A × B) = A)
 
Theoremdmxpid 4924 The domain of a square cross product. (Contributed by set.mm contributors, 28-Jul-1995.)
dom (A × A) = A
 
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.)
dom ((A × A) ∩ (B × B)) = (AB)
 
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.)
((A × A) = (B × B) ↔ A = B)
 
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.)
(B A Proj1 B dom A)
 
Theoremreseq1 4928 Equality theorem for restrictions. (Contributed by set.mm contributors, 7-Aug-1994.)
(A = B → (A C) = (B C))
 
Theoremreseq2 4929 Equality theorem for restrictions. (Contributed by set.mm contributors, 8-Aug-1994.)
(A = B → (C A) = (C B))
 
Theoremreseq1i 4930 Equality inference for restrictions. (Contributed by set.mm contributors, 21-Oct-2014.)
A = B       (A C) = (B C)
 
Theoremreseq2i 4931 Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
A = B       (C A) = (C B)
 
Theoremreseq12i 4932 Equality inference for restrictions. (Contributed by set.mm contributors, 21-Oct-2014.)
A = B    &   C = D       (A C) = (B D)
 
Theoremreseq1d 4933 Equality deduction for restrictions. (Contributed by set.mm contributors, 21-Oct-2014.)
(φA = B)       (φ → (A C) = (B C))
 
Theoremreseq2d 4934 Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
(φA = B)       (φ → (C A) = (C B))
 
Theoremreseq12d 4935 Equality deduction for restrictions. (Contributed by set.mm contributors, 21-Oct-2014.)
(φA = B)    &   (φC = D)       (φ → (A C) = (B D))
 
Theoremnfres 4936 Bound-variable hypothesis builder for restriction. (Contributed by NM, 15-Sep-2003.) (Revised by David Abernethy, 19-Jun-2012.)
xA    &   xB       x(A B)
 
Theoremimaeq1 4937 Equality theorem for image. (Contributed by set.mm contributors, 14-Aug-1994.)
(A = B → (AC) = (BC))
 
Theoremimaeq2 4938 Equality theorem for image. (Contributed by set.mm contributors, 14-Aug-1994.)
(A = B → (CA) = (CB))
 
Theoremimaeq1i 4939 Equality theorem for image. (Contributed by set.mm contributors, 21-Dec-2008.)
A = B       (AC) = (BC)
 
Theoremimaeq2i 4940 Equality theorem for image. (Contributed by set.mm contributors, 21-Dec-2008.)
A = B       (CA) = (CB)
 
Theoremimaeq1d 4941 Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
(φA = B)       (φ → (AC) = (BC))
 
Theoremimaeq2d 4942 Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
(φA = B)       (φ → (CA) = (CB))
 
Theoremimaeq12d 4943 Equality theorem for image. (Contributed by SF, 8-Jan-2018.)
(φA = B)    &   (φC = D)       (φ → (AC) = (BD))
 
Theoremelimapw1 4944* Membership in an image under a unit power class. (Contributed by set.mm contributors, 19-Feb-2015.)
(A (B1C) ↔ x C {x}, A B)
 
Theoremelimapw12 4945* Membership in an image under two unit power classes. (Contributed by set.mm contributors, 18-Mar-2015.)
(A (B11C) ↔ x C {{x}}, A B)
 
Theoremelimapw13 4946* Membership in an image under three unit power classes. (Contributed by set.mm contributors, 18-Mar-2015.)
(A (B111C) ↔ x C {{{x}}}, A B)
 
Theoremelima1c 4947* Membership in an image under cardinal one. (Contributed by set.mm contributors, 6-Feb-2015.)
(A (B “ 1c) ↔ x{x}, A B)
 
Theoremelimapw11c 4948* Membership in an image under the unit power class of cardinal one. (Contributed by set.mm contributors, 25-Feb-2015.)
(A (B11c) ↔ x{{x}}, A B)
 
Theorembrres 4949 Binary relation on a restriction. (Contributed by set.mm contributors, 12-Dec-2006.)
(A(C D)B ↔ (ACB A D))
 
Theoremopelres 4950 Ordered pair membership in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by set.mm contributors, 13-Nov-1995.)
(A, B (C D) ↔ (A, B C A D))
 
Theoremdfima3 4951 Alternate definition of image. (Contributed by set.mm contributors, 19-Apr-2004.) (Revised by set.mm contributors, 27-Aug-2011.)
(AB) = ran (A B)
 
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.)
(AB) = {y x(x B x, y A)}
 
Theoremnfima 4953 Bound-variable hypothesis builder for image. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
xA    &   xB       x(AB)
 
Theoremnfimad 4954 Deduction version of bound-variable hypothesis builder nfima 4953. (Contributed by FL, 15-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
(φxA)    &   (φxB)       (φx(AB))
 
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.)
(A C[A / x](FB) = ([A / x]F[A / x]B))
 
Theoremrneq 4956 Equality theorem for range. (Contributed by set.mm contributors, 29-Dec-1996.)
(A = B → ran A = ran B)
 
Theoremrneqi 4957 Equality inference for range. (Contributed by set.mm contributors, 4-Mar-2004.)
A = B       ran A = ran B
 
Theoremrneqd 4958 Equality deduction for range. (Contributed by set.mm contributors, 4-Mar-2004.)
(φA = B)       (φ → ran A = ran B)
 
Theoremrnss 4959 Subset theorem for range. (Contributed by set.mm contributors, 22-Mar-1998.)
(A B → ran A ran B)
 
Theorembrelrn 4960 The second argument of a binary relation belongs to its range. (Contributed by set.mm contributors, 29-Jun-2008.)
(ACBB ran C)
 
Theoremopelrn 4961 Membership of second member of an ordered pair in a range. (Contributed by set.mm contributors, 8-Jan-2015.)
(A, B CB ran C)
 
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.)
xA    &   yA       ran A = {y x xAy}
 
Theoremnfrn 4963 Bound-variable hypothesis builder for range. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.)
xA       xran A
 
Theoremnfdm 4964 Bound-variable hypothesis builder for domain. (Contributed by NM, 30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
xA       xdom A
 
Theoremdmiin 4965 Domain of an intersection. (Contributed by FL, 15-Oct-2012.)
dom x A B x A dom B
 
Theoremcsbrng 4966 Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.)
(A V[A / x]ran B = ran [A / x]B)
 
Theoremrnopab 4967* The range of a class of ordered pairs. (Contributed by NM, 14-Aug-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
ran {x, y φ} = {y xφ}
 
Theoremrnopab2 4968* The range of a function expressed as a class abstraction. (Contributed by set.mm contributors, 23-Mar-2006.)
ran {x, y (x A y = B)} = {y x A y = B}
 
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.)
ran =
 
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.)
(A = ↔ ran A = )
 
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.)
dom (A B) dom B
 
Theoremrncoss 4972 Range of a composition. (Contributed by set.mm contributors, 19-Mar-1998.)
ran (A B) ran A
 
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.)
(ran B dom A → dom (A B) = dom B)
 
Theoremdmcoeq 4974 Domain of a composition. (Contributed by set.mm contributors, 19-Mar-1998.)
(dom A = ran B → dom (A B) = dom B)
 
Theoremrncoeq 4975 Range of a composition. (Contributed by set.mm contributors, 19-Mar-1998.)
(dom A = ran B → ran (A B) = ran A)
 
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.)
(A V[A / x](B C) = ([A / x]B [A / x]C))
 
Theoremres0 4977 A restriction to the empty set is empty. (Contributed by set.mm contributors, 12-Nov-1994.)
(A ) =
 
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.)
(A D → (A, B (C D) ↔ A, B C))
 
Theoremresieq 4979 A restricted identity relation is equivalent to equality in its domain. (Contributed by set.mm contributors, 30-Apr-2004.)
(B A → (B( I A)CB = C))
 
Theoremresres 4980 The restriction of a restriction. (Contributed by set.mm contributors, 27-Mar-2008.)
((A B) C) = (A (BC))
 
Theoremresundi 4981 Distributive law for restriction over union. Theorem 31 of [Suppes] p. 65. (Contributed by set.mm contributors, 30-Sep-2002.)
(A (BC)) = ((A B) ∪ (A C))
 
Theoremresundir 4982 Distributive law for restriction over union. (Contributed by set.mm contributors, 23-Sep-2004.)
((AB) C) = ((A C) ∪ (B C))
 
Theoremresindi 4983 Class restriction distributes over intersection. (Contributed by FL, 6-Oct-2008.)
(A (BC)) = ((A B) ∩ (A C))
 
Theoremresindir 4984 Class restriction distributes over intersection. (Contributed by set.mm contributors, 18-Dec-2008.)
((AB) C) = ((A C) ∩ (B C))
 
Theoreminres 4985 Move intersection into class restriction. (Contributed by set.mm contributors, 18-Dec-2008.)
(A ∩ (B C)) = ((AB) C)
 
Theoremdmres 4986 The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25. (Contributed by set.mm contributors, 1-Aug-1994.)
dom (A B) = (B ∩ dom A)
 
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.)
(A dom B ↔ dom (B A) = A)
 
Theoremresss 4988 A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25. (Contributed by set.mm contributors, 2-Aug-1994.)
(A B) A
 
Theoremrescom 4989 Commutative law for restriction. (Contributed by set.mm contributors, 27-Mar-1998.)
((A B) C) = ((A C) B)
 
Theoremssres 4990 Subclass theorem for restriction. (Contributed by set.mm contributors, 16-Aug-1994.)
(A B → (A C) (B C))
 
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.)
(A B → (C A) (C B))
 
Theoremresabs1 4992 Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25. (Contributed by set.mm contributors, 9-Aug-1994.)
(B C → ((A C) B) = (A B))
 
Theoremresabs2 4993 Absorption law for restriction. (Contributed by set.mm contributors, 27-Mar-1998.)
(B C → ((A B) C) = (A B))
 
Theoremresidm 4994 Idempotent law for restriction. (Contributed by set.mm contributors, 27-Mar-1998.)
((A B) B) = (A B)
 
Theoremelres 4995* Membership in a restriction. (Contributed by Scott Fenton, 17-Mar-2011.)
(A (B C) ↔ x C y(A = x, y x, y B))
 
Theoremelsnres 4996* Memebership in restriction to a singleton. (Contributed by Scott Fenton, 17-Mar-2011.)
C V       (A (B {C}) ↔ y(A = C, y C, y B))
 
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.)
(dom A B → (A B) = A)
 
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.)
(A dom A) = A
 
Theoremresopab 4999* Restriction of a class abstraction of ordered pairs. (Contributed by set.mm contributors, 5-Nov-2002.)
({x, y φ} A) = {x, y (x A φ)}
 
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.)
(A I ↔ A = ( I dom A))
    < 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 >