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 ∣ ∃y⟨x, y⟩ ∈ 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 ∣ ∃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 ∣ ∃x⟨x, y⟩ ∈ 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.)
⊢ ℲxA    &   ⊢ ℲyA    ⇒   ⊢ dom A = {x ∣ ∃y xAy}
Theorem	dmss 4906	Subset theorem for domain. (Contributed by set.mm contributors, 11-Aug-1994.)
⊢ (A ⊆ B → dom A ⊆ 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.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → 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⟩ ∈ C → A ∈ 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 ∈ 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 ∪ B) = (dom A ∪ 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 ∩ B) ⊆ (dom A ∩ 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 ∪A = ∪x ∈ 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⟩ ∣ φ} = {x ∣ ∃yφ}
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 ∈ A ∧ φ)} ⊆ A
Theorem	dmopab3 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)
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 × B) = A)
Theorem	dmxpid 4924	The domain of a square cross product. (Contributed by set.mm contributors, 28-Jul-1995.)
⊢ dom (A × 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 × A) ∩ (B × B)) = (A ∩ 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 × A) = (B × 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 ∈ A → Proj1 B ∈ 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.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ↾ C) = (B ↾ C))
Theorem	reseq2d 4934	Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C ↾ A) = (C ↾ B))
Theorem	reseq12d 4935	Equality deduction for restrictions. (Contributed by set.mm contributors, 21-Oct-2014.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (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.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎ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.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A “ C) = (B “ C))
Theorem	imaeq2d 4942	Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C “ A) = (C “ B))
Theorem	imaeq12d 4943	Equality theorem for image. (Contributed by SF, 8-Jan-2018.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (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 ∈ (B “ ℘1C) ↔ ∃x ∈ C ⟨{x}, A⟩ ∈ B)
Theorem	elimapw12 4945*	Membership in an image under two unit power classes. (Contributed by set.mm contributors, 18-Mar-2015.)
⊢ (A ∈ (B “ ℘1℘1C) ↔ ∃x ∈ C ⟨{{x}}, A⟩ ∈ B)
Theorem	elimapw13 4946*	Membership in an image under three unit power classes. (Contributed by set.mm contributors, 18-Mar-2015.)
⊢ (A ∈ (B “ ℘1℘1℘1C) ↔ ∃x ∈ C ⟨{{{x}}}, A⟩ ∈ B)
Theorem	elima1c 4947*	Membership in an image under cardinal one. (Contributed by set.mm contributors, 6-Feb-2015.)
⊢ (A ∈ (B “ 1c) ↔ ∃x⟨{x}, A⟩ ∈ 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 ∈ (B “ ℘11c) ↔ ∃x⟨{{x}}, A⟩ ∈ B)
Theorem	brres 4949	Binary relation on a restriction. (Contributed by set.mm contributors, 12-Dec-2006.)
⊢ (A(C ↾ D)B ↔ (ACB ∧ A ∈ 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⟩ ∈ (C ↾ D) ↔ (⟨A, B⟩ ∈ C ∧ A ∈ 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 ∣ ∃x(x ∈ B ∧ ⟨x, y⟩ ∈ A)}
Theorem	nfima 4953	Bound-variable hypothesis builder for image. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎ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.)
⊢ (φ → ℲxA)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → Ⅎ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 ∈ 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.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → ran A = ran B)
Theorem	rnss 4959	Subset theorem for range. (Contributed by set.mm contributors, 22-Mar-1998.)
⊢ (A ⊆ B → ran A ⊆ 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 ∈ 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⟩ ∈ C → B ∈ 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.)
⊢ ℲxA    &   ⊢ ℲyA    ⇒   ⊢ ran A = {y ∣ ∃x xAy}
Theorem	nfrn 4963	Bound-variable hypothesis builder for range. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ ℲxA    ⇒   ⊢ Ⅎxran A
Theorem	nfdm 4964	Bound-variable hypothesis builder for domain. (Contributed by NM, 30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ ℲxA    ⇒   ⊢ Ⅎxdom A
Theorem	dmiin 4965	Domain of an intersection. (Contributed by FL, 15-Oct-2012.)
⊢ dom ∩x ∈ A B ⊆ ∩x ∈ A dom B
Theorem	csbrng 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)
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⟩ ∣ φ} = {y ∣ ∃xφ}
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 ∈ A ∧ y = B)} = {y ∣ ∃x ∈ 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 ∘ B) ⊆ dom B
Theorem	rncoss 4972	Range of a composition. (Contributed by set.mm contributors, 19-Mar-1998.)
⊢ ran (A ∘ B) ⊆ 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 ⊆ dom A → dom (A ∘ B) = dom B)
Theorem	dmcoeq 4974	Domain of a composition. (Contributed by set.mm contributors, 19-Mar-1998.)
⊢ (dom A = ran B → dom (A ∘ B) = dom B)
Theorem	rncoeq 4975	Range of a composition. (Contributed by set.mm contributors, 19-Mar-1998.)
⊢ (dom A = ran B → ran (A ∘ 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 ∈ 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 ∈ D → (⟨A, B⟩ ∈ (C ↾ D) ↔ ⟨A, B⟩ ∈ C))
Theorem	resieq 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)C ↔ B = C))
Theorem	resres 4980	The restriction of a restriction. (Contributed by set.mm contributors, 27-Mar-2008.)
⊢ ((A ↾ B) ↾ C) = (A ↾ (B ∩ 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 ∪ C)) = ((A ↾ B) ∪ (A ↾ C))
Theorem	resundir 4982	Distributive law for restriction over union. (Contributed by set.mm contributors, 23-Sep-2004.)
⊢ ((A ∪ B) ↾ C) = ((A ↾ C) ∪ (B ↾ C))
Theorem	resindi 4983	Class restriction distributes over intersection. (Contributed by FL, 6-Oct-2008.)
⊢ (A ↾ (B ∩ C)) = ((A ↾ B) ∩ (A ↾ C))
Theorem	resindir 4984	Class restriction distributes over intersection. (Contributed by set.mm contributors, 18-Dec-2008.)
⊢ ((A ∩ B) ↾ C) = ((A ↾ C) ∩ (B ↾ C))
Theorem	inres 4985	Move intersection into class restriction. (Contributed by set.mm contributors, 18-Dec-2008.)
⊢ (A ∩ (B ↾ C)) = ((A ∩ 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 ∩ 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 ⊆ 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) ⊆ 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 ⊆ B → (A ↾ 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 ⊆ B → (C ↾ A) ⊆ (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 → ((A ↾ C) ↾ B) = (A ↾ B))
Theorem	resabs2 4993	Absorption law for restriction. (Contributed by set.mm contributors, 27-Mar-1998.)
⊢ (B ⊆ 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 ∈ (B ↾ C) ↔ ∃x ∈ C ∃y(A = ⟨x, y⟩ ∧ ⟨x, y⟩ ∈ B))
Theorem	elsnres 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))
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 ⊆ 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⟩ ∣ φ} ↾ A) = {⟨x, y⟩ ∣ (x ∈ A ∧ φ)}
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 ⊆ I ↔ A = ( I ↾ dom A))