P. 50 of Theorem List - New Foundations Explorer

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.)
|- dom A = {x | E.y<.x, y>. e. A}
Theorem	dfrn2 4902*	Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by set.mm contributors, 27-Dec-1996.)
|- ran A = {y | E.x xAy}
Theorem	dfrn3 4903*	Alternate definition of range. Definition 6.5(2) of [TakeutiZaring] p. 24. (Contributed by set.mm contributors, 28-Dec-1996.)
|- ran A = {y | E.x<.x, y>. e. A}
Theorem	dfrn4 4904	Alternate definition of range. (Contributed by set.mm contributors, 5-Feb-2015.)
|- ran A = dom `'A
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.)
|- F/_xA   &   |- F/_yA   =>   |- dom A = {x | E.y xAy}
Theorem	dmss 4906	Subset theorem for domain. (Contributed by set.mm contributors, 11-Aug-1994.)
|- (A C_ B -> dom A C_ dom B)
Theorem	dmeq 4907	Equality theorem for domain. (Contributed by set.mm contributors, 11-Aug-1994.)
|- (A = B -> dom A = dom B)
Theorem	dmeqi 4908	Equality inference for domain. (Contributed by set.mm contributors, 4-Mar-2004.)
|- A = B   =>   |- dom A = dom B
Theorem	dmeqd 4909	Equality deduction for domain. (Contributed by set.mm contributors, 4-Mar-2004.)
|- (ph -> A = B)   =>   |- (ph -> dom A = dom B)
Theorem	opeldm 4910	Membership of first of an ordered pair in a domain. (Contributed by set.mm contributors, 30-Jul-1995.)
|- (<.A, B>. e. C -> A e. dom C)
Theorem	breldm 4911	Membership of first of a binary relation in a domain. (Contributed by set.mm contributors, 8-Jan-2015.)
|- (ARB -> A e. dom R)
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.)
|- dom (A u. B) = (dom A u. dom B)
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.)
|- dom (A i^i B) C_ (dom A i^i dom B)
Theorem	dmuni 4914*	The domain of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by set.mm contributors, 3-Feb-2004.)
|- dom U.A = U_x e. A dom x
Theorem	dmopab 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>. | ph} = {x | E.yph}
Theorem	dmopabss 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 e. A /\ ph)} C_ A
Theorem	dmopab3 4917*	The domain of a restricted class of ordered pairs. (Contributed by set.mm contributors, 31-Jan-2004.)
|- (A.x e. A E.yph <-> dom {<.x, y>. | (x e. A /\ ph)} = A)
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.)
|- dom (/) = (/)
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.)
|- dom _I = _V
Theorem	dmv 4920	The domain of the universe is the universe. (Contributed by set.mm contributors, 8-Aug-2003.)
|- dom _V = _V
Theorem	dm0rn0 4921	An empty domain implies an empty range. (Contributed by set.mm contributors, 21-May-1998.)
|- (dom A = (/) <-> ran A = (/))
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.)
|- (A = (/) <-> dom A = (/))
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.)
|- (B =/= (/) -> dom (A X. B) = A)
Theorem	dmxpid 4924	The domain of a square cross product. (Contributed by set.mm contributors, 28-Jul-1995.)
|- dom (A X. A) = A
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.)
|- dom ((A X. A) i^i (B X. B)) = (A i^i B)
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.)
|- ((A X. A) = (B X. B) <-> A = B)
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.)
|- (B e. A -> Proj1 B e. dom A)
Theorem	reseq1 4928	Equality theorem for restrictions. (Contributed by set.mm contributors, 7-Aug-1994.)
|- (A = B -> (A |` C) = (B |` C))
Theorem	reseq2 4929	Equality theorem for restrictions. (Contributed by set.mm contributors, 8-Aug-1994.)
|- (A = B -> (C |` A) = (C |` B))
Theorem	reseq1i 4930	Equality inference for restrictions. (Contributed by set.mm contributors, 21-Oct-2014.)
|- A = B   =>   |- (A |` C) = (B |` C)
Theorem	reseq2i 4931	Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
|- A = B   =>   |- (C |` A) = (C |` B)
Theorem	reseq12i 4932	Equality inference for restrictions. (Contributed by set.mm contributors, 21-Oct-2014.)
|- A = B   &   |- C = D   =>   |- (A |` C) = (B |` D)
Theorem	reseq1d 4933	Equality deduction for restrictions. (Contributed by set.mm contributors, 21-Oct-2014.)
|- (ph -> A = B)   =>   |- (ph -> (A |` C) = (B |` C))
Theorem	reseq2d 4934	Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
|- (ph -> A = B)   =>   |- (ph -> (C |` A) = (C |` B))
Theorem	reseq12d 4935	Equality deduction for restrictions. (Contributed by set.mm contributors, 21-Oct-2014.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (A |` C) = (B |` D))
Theorem	nfres 4936	Bound-variable hypothesis builder for restriction. (Contributed by NM, 15-Sep-2003.) (Revised by David Abernethy, 19-Jun-2012.)
|- F/_xA   &   |- F/_xB   =>   |- F/_x(A |` B)
Theorem	imaeq1 4937	Equality theorem for image. (Contributed by set.mm contributors, 14-Aug-1994.)
|- (A = B -> (A"C) = (B"C))
Theorem	imaeq2 4938	Equality theorem for image. (Contributed by set.mm contributors, 14-Aug-1994.)
|- (A = B -> (C"A) = (C"B))
Theorem	imaeq1i 4939	Equality theorem for image. (Contributed by set.mm contributors, 21-Dec-2008.)
|- A = B   =>   |- (A"C) = (B"C)
Theorem	imaeq2i 4940	Equality theorem for image. (Contributed by set.mm contributors, 21-Dec-2008.)
|- A = B   =>   |- (C"A) = (C"B)
Theorem	imaeq1d 4941	Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
|- (ph -> A = B)   =>   |- (ph -> (A"C) = (B"C))
Theorem	imaeq2d 4942	Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
|- (ph -> A = B)   =>   |- (ph -> (C"A) = (C"B))
Theorem	imaeq12d 4943	Equality theorem for image. (Contributed by SF, 8-Jan-2018.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (A"C) = (B"D))
Theorem	elimapw1 4944*	Membership in an image under a unit power class. (Contributed by set.mm contributors, 19-Feb-2015.)
|- (A e. (B"~P1 C) <-> E.x e. C <.{x}, A>. e. B)
Theorem	elimapw12 4945*	Membership in an image under two unit power classes. (Contributed by set.mm contributors, 18-Mar-2015.)
|- (A e. (B"~P1 ~P1 C) <-> E.x e. C <.{{x}}, A>. e. B)
Theorem	elimapw13 4946*	Membership in an image under three unit power classes. (Contributed by set.mm contributors, 18-Mar-2015.)
|- (A e. (B"~P1 ~P1 ~P1 C) <-> E.x e. C <.{{{x}}}, A>. e. B)
Theorem	elima1c 4947*	Membership in an image under cardinal one. (Contributed by set.mm contributors, 6-Feb-2015.)
|- (A e. (B"1c) <-> E.x<.{x}, A>. e. B)
Theorem	elimapw11c 4948*	Membership in an image under the unit power class of cardinal one. (Contributed by set.mm contributors, 25-Feb-2015.)
|- (A e. (B"~P1 1c) <-> E.x<.{{x}}, A>. e. B)
Theorem	brres 4949	Binary relation on a restriction. (Contributed by set.mm contributors, 12-Dec-2006.)
|- (A(C |` D)B <-> (ACB /\ A e. D))
Theorem	opelres 4950	Ordered pair membership in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by set.mm contributors, 13-Nov-1995.)
|- (<.A, B>. e. (C |` D) <-> (<.A, B>. e. C /\ A e. D))
Theorem	dfima3 4951	Alternate definition of image. (Contributed by set.mm contributors, 19-Apr-2004.) (Revised by set.mm contributors, 27-Aug-2011.)
|- (A"B) = ran (A |` B)
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.)
|- (A"B) = {y | E.x(x e. B /\ <.x, y>. e. A)}
Theorem	nfima 4953	Bound-variable hypothesis builder for image. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- F/_xA   &   |- F/_xB   =>   |- F/_x(A"B)
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.)
|- (ph -> F/_xA)   &   |- (ph -> F/_xB)   =>   |- (ph -> F/_x(A"B))
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.)
|- (A e. C -> [_A / x]_(F"B) = ([_A / x]_F"[_A / x]_B))
Theorem	rneq 4956	Equality theorem for range. (Contributed by set.mm contributors, 29-Dec-1996.)
|- (A = B -> ran A = ran B)
Theorem	rneqi 4957	Equality inference for range. (Contributed by set.mm contributors, 4-Mar-2004.)
|- A = B   =>   |- ran A = ran B
Theorem	rneqd 4958	Equality deduction for range. (Contributed by set.mm contributors, 4-Mar-2004.)
|- (ph -> A = B)   =>   |- (ph -> ran A = ran B)
Theorem	rnss 4959	Subset theorem for range. (Contributed by set.mm contributors, 22-Mar-1998.)
|- (A C_ B -> ran A C_ ran B)
Theorem	brelrn 4960	The second argument of a binary relation belongs to its range. (Contributed by set.mm contributors, 29-Jun-2008.)
|- (ACB -> B e. ran C)
Theorem	opelrn 4961	Membership of second member of an ordered pair in a range. (Contributed by set.mm contributors, 8-Jan-2015.)
|- (<.A, B>. e. C -> B e. ran C)
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.)
|- F/_xA   &   |- F/_yA   =>   |- ran A = {y | E.x xAy}
Theorem	nfrn 4963	Bound-variable hypothesis builder for range. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_xA   =>   |- F/_xran A
Theorem	nfdm 4964	Bound-variable hypothesis builder for domain. (Contributed by NM, 30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_xA   =>   |- F/_xdom A
Theorem	dmiin 4965	Domain of an intersection. (Contributed by FL, 15-Oct-2012.)
|- dom |^|_x e. A B C_ |^|_x e. A dom B
Theorem	csbrng 4966	Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.)
|- (A e. V -> [_A / x]_ran B = ran [_A / x]_B)
Theorem	rnopab 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>. | ph} = {y | E.xph}
Theorem	rnopab2 4968*	The range of a function expressed as a class abstraction. (Contributed by set.mm contributors, 23-Mar-2006.)
|- ran {<.x, y>. | (x e. A /\ y = B)} = {y | E.x e. A y = B}
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.)
|- ran (/) = (/)
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.)
|- (A = (/) <-> ran A = (/))
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.)
|- dom (A o. B) C_ dom B
Theorem	rncoss 4972	Range of a composition. (Contributed by set.mm contributors, 19-Mar-1998.)
|- ran (A o. B) C_ ran A
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.)
|- (ran B C_ dom A -> dom (A o. B) = dom B)
Theorem	dmcoeq 4974	Domain of a composition. (Contributed by set.mm contributors, 19-Mar-1998.)
|- (dom A = ran B -> dom (A o. B) = dom B)
Theorem	rncoeq 4975	Range of a composition. (Contributed by set.mm contributors, 19-Mar-1998.)
|- (dom A = ran B -> ran (A o. B) = ran A)
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.)
|- (A e. V -> [_A / x]_(B |` C) = ([_A / x]_B |` [_A / x]_C))
Theorem	res0 4977	A restriction to the empty set is empty. (Contributed by set.mm contributors, 12-Nov-1994.)
|- (A |` (/)) = (/)
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.)
|- (A e. D -> (<.A, B>. e. (C |` D) <-> <.A, B>. e. C))
Theorem	resieq 4979	A restricted identity relation is equivalent to equality in its domain. (Contributed by set.mm contributors, 30-Apr-2004.)
|- (B e. A -> (B( _I |` A)C <-> B = C))
Theorem	resres 4980	The restriction of a restriction. (Contributed by set.mm contributors, 27-Mar-2008.)
|- ((A |` B) |` C) = (A |` (B i^i C))
Theorem	resundi 4981	Distributive law for restriction over union. Theorem 31 of [Suppes] p. 65. (Contributed by set.mm contributors, 30-Sep-2002.)
|- (A |` (B u. C)) = ((A |` B) u. (A |` C))
Theorem	resundir 4982	Distributive law for restriction over union. (Contributed by set.mm contributors, 23-Sep-2004.)
|- ((A u. B) |` C) = ((A |` C) u. (B |` C))
Theorem	resindi 4983	Class restriction distributes over intersection. (Contributed by FL, 6-Oct-2008.)
|- (A |` (B i^i C)) = ((A |` B) i^i (A |` C))
Theorem	resindir 4984	Class restriction distributes over intersection. (Contributed by set.mm contributors, 18-Dec-2008.)
|- ((A i^i B) |` C) = ((A |` C) i^i (B |` C))
Theorem	inres 4985	Move intersection into class restriction. (Contributed by set.mm contributors, 18-Dec-2008.)
|- (A i^i (B |` C)) = ((A i^i B) |` C)
Theorem	dmres 4986	The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25. (Contributed by set.mm contributors, 1-Aug-1994.)
|- dom (A |` B) = (B i^i dom A)
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.)
|- (A C_ dom B <-> dom (B |` A) = A)
Theorem	resss 4988	A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25. (Contributed by set.mm contributors, 2-Aug-1994.)
|- (A |` B) C_ A
Theorem	rescom 4989	Commutative law for restriction. (Contributed by set.mm contributors, 27-Mar-1998.)
|- ((A |` B) |` C) = ((A |` C) |` B)
Theorem	ssres 4990	Subclass theorem for restriction. (Contributed by set.mm contributors, 16-Aug-1994.)
|- (A C_ B -> (A |` C) C_ (B |` C))
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.)
|- (A C_ B -> (C |` A) C_ (C |` B))
Theorem	resabs1 4992	Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25. (Contributed by set.mm contributors, 9-Aug-1994.)
|- (B C_ C -> ((A |` C) |` B) = (A |` B))
Theorem	resabs2 4993	Absorption law for restriction. (Contributed by set.mm contributors, 27-Mar-1998.)
|- (B C_ C -> ((A |` B) |` C) = (A |` B))
Theorem	residm 4994	Idempotent law for restriction. (Contributed by set.mm contributors, 27-Mar-1998.)
|- ((A |` B) |` B) = (A |` B)
Theorem	elres 4995*	Membership in a restriction. (Contributed by Scott Fenton, 17-Mar-2011.)
|- (A e. (B |` C) <-> E.x e. C E.y(A = <.x, y>. /\ <.x, y>. e. B))
Theorem	elsnres 4996*	Memebership in restriction to a singleton. (Contributed by Scott Fenton, 17-Mar-2011.)
|- C e. _V   =>   |- (A e. (B |` {C}) <-> E.y(A = <.C, y>. /\ <.C, y>. e. B))
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.)
|- (dom A C_ B -> (A |` B) = A)
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.)
|- (A |` dom A) = A
Theorem	resopab 4999*	Restriction of a class abstraction of ordered pairs. (Contributed by set.mm contributors, 5-Nov-2002.)
|- ({<.x, y>. | ph} |` A) = {<.x, y>. | (x e. A /\ ph)}
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.)
|- (A C_ _I <-> A = ( _I |` dom A))