P. 50 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4901-5000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	releldm 4901	The first argument of a binary relation belongs to its domain. (Contributed by NM, 2-Jul-2008.)
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
Theorem	relelrn 4902	The second argument of a binary relation belongs to its range. (Contributed by NM, 2-Jul-2008.)
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ ran 𝑅)
Theorem	releldmb 4903*	Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015.)
⊢ (Rel 𝑅 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥))
Theorem	relelrnb 4904*	Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015.)
⊢ (Rel 𝑅 → (𝐴 ∈ ran 𝑅 ↔ ∃𝑥 𝑥𝑅𝐴))
Theorem	releldmi 4905	The first argument of a binary relation belongs to its domain. (Contributed by NM, 28-Apr-2015.)
⊢ Rel 𝑅    ⇒   ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)
Theorem	relelrni 4906	The second argument of a binary relation belongs to its range. (Contributed by NM, 28-Apr-2015.)
⊢ Rel 𝑅    ⇒   ⊢ (𝐴𝑅𝐵 → 𝐵 ∈ ran 𝑅)
Theorem	dfrnf 4907*	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.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
Theorem	elrn2 4908*	Membership in a range. (Contributed by NM, 10-Jul-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥⟨𝑥, 𝐴⟩ ∈ 𝐵)
Theorem	elrn 4909*	Membership in a range. (Contributed by NM, 2-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴)
Theorem	nfdm 4910	Bound-variable hypothesis builder for domain. (Contributed by NM, 30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥dom 𝐴
Theorem	nfrn 4911	Bound-variable hypothesis builder for range. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥ran 𝐴
Theorem	dmiin 4912	Domain of an intersection. (Contributed by FL, 15-Oct-2012.)
⊢ dom ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 dom 𝐵
Theorem	rnopab 4913*	The range of a class of ordered pairs. (Contributed by NM, 14-Aug-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
⊢ ran {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑦 ∣ ∃𝑥𝜑}
Theorem	rnmpt 4914*	The range of a function in maps-to notation. (Contributed by Scott Fenton, 21-Mar-2011.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}
Theorem	elrnmpt 4915*	The range of a function in maps-to notation. (Contributed by Mario Carneiro, 20-Feb-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))
Theorem	elrnmpt1s 4916*	Elementhood in an image set. (Contributed by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹)
Theorem	elrnmpt1 4917	Elementhood in an image set. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ ran 𝐹)
Theorem	elrnmptg 4918*	Membership in the range of a function. (Contributed by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))
Theorem	elrnmpti 4919*	Membership in the range of a function. (Contributed by NM, 30-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)
Theorem	elrnmptdv 4920*	Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐷 ∈ ran 𝐹)
Theorem	elrnmpt2d 4921*	Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ ran 𝐹)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)
Theorem	rn0 4922	The range of the empty set is empty. Part of Theorem 3.8(v) of [Monk1] p. 36. (Contributed by NM, 4-Jul-1994.)
⊢ ran ∅ = ∅
Theorem	dfiun3g 4923	Alternate definition of indexed union when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵))
Theorem	dfiin3g 4924	Alternate definition of indexed intersection when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ ran (𝑥 ∈ 𝐴 ↦ 𝐵))
Theorem	dfiun3 4925	Alternate definition of indexed union when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	dfiin3 4926	Alternate definition of indexed intersection when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ ran (𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	riinint 4927*	Express a relative indexed intersection as an intersection. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋) → (𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆) = ∩ ({𝑋} ∪ ran (𝑘 ∈ 𝐼 ↦ 𝑆)))
Theorem	relrn0 4928	A relation is empty iff its range is empty. (Contributed by NM, 15-Sep-2004.)
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ran 𝐴 = ∅))
Theorem	dmrnssfld 4929	The domain and range of a class are included in its double union. (Contributed by NM, 13-May-2008.)
⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
Theorem	dmexg 4930	The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Apr-1995.)
⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
Theorem	rnexg 4931	The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 31-Mar-1995.)
⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
Theorem	dmex 4932	The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Jul-2008.)
⊢ 𝐴 ∈ V    ⇒   ⊢ dom 𝐴 ∈ V
Theorem	rnex 4933	The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 7-Jul-2008.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ran 𝐴 ∈ V
Theorem	iprc 4934	The identity function is a proper class. This means, for example, that we cannot use it as a member of the class of continuous functions unless it is restricted to a set. (Contributed by NM, 1-Jan-2007.)
⊢ ¬ I ∈ V
Theorem	dmcoss 4935	Domain of a composition. Theorem 21 of [Suppes] p. 63. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ dom (𝐴 ∘ 𝐵) ⊆ dom 𝐵
Theorem	rncoss 4936	Range of a composition. (Contributed by NM, 19-Mar-1998.)
⊢ ran (𝐴 ∘ 𝐵) ⊆ ran 𝐴
Theorem	dmcosseq 4937	Domain of a composition. (Contributed by NM, 28-May-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (ran 𝐵 ⊆ dom 𝐴 → dom (𝐴 ∘ 𝐵) = dom 𝐵)
Theorem	dmcoeq 4938	Domain of a composition. (Contributed by NM, 19-Mar-1998.)
⊢ (dom 𝐴 = ran 𝐵 → dom (𝐴 ∘ 𝐵) = dom 𝐵)
Theorem	rncoeq 4939	Range of a composition. (Contributed by NM, 19-Mar-1998.)
⊢ (dom 𝐴 = ran 𝐵 → ran (𝐴 ∘ 𝐵) = ran 𝐴)
Theorem	reseq1 4940	Equality theorem for restrictions. (Contributed by NM, 7-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
Theorem	reseq2 4941	Equality theorem for restrictions. (Contributed by NM, 8-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
Theorem	reseq1i 4942	Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)
Theorem	reseq2i 4943	Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)
Theorem	reseq12i 4944	Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷)
Theorem	reseq1d 4945	Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
Theorem	reseq2d 4946	Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
Theorem	reseq12d 4947	Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷))
Theorem	nfres 4948	Bound-variable hypothesis builder for restriction. (Contributed by NM, 15-Sep-2003.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)
Theorem	csbresg 4949	Distribute proper substitution through the restriction of a class. (Contributed by Alan Sare, 10-Nov-2012.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶))
Theorem	res0 4950	A restriction to the empty set is empty. (Contributed by NM, 12-Nov-1994.)
⊢ (𝐴 ↾ ∅) = ∅
Theorem	opelres 4951	Ordered pair membership in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by NM, 13-Nov-1995.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 ↾ 𝐷) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝐶 ∧ 𝐴 ∈ 𝐷))
Theorem	brres 4952	Binary relation on a restriction. (Contributed by NM, 12-Dec-2006.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴(𝐶 ↾ 𝐷)𝐵 ↔ (𝐴𝐶𝐵 ∧ 𝐴 ∈ 𝐷))
Theorem	opelresg 4953	Ordered pair membership in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by NM, 14-Oct-2005.)
⊢ (𝐵 ∈ 𝑉 → (⟨𝐴, 𝐵⟩ ∈ (𝐶 ↾ 𝐷) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝐶 ∧ 𝐴 ∈ 𝐷)))
Theorem	brresg 4954	Binary relation on a restriction. (Contributed by Mario Carneiro, 4-Nov-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴(𝐶 ↾ 𝐷)𝐵 ↔ (𝐴𝐶𝐵 ∧ 𝐴 ∈ 𝐷)))
Theorem	opres 4955	Ordered pair membership in a restriction when the first member belongs to the restricting class. (Contributed by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐷 → (⟨𝐴, 𝐵⟩ ∈ (𝐶 ↾ 𝐷) ↔ ⟨𝐴, 𝐵⟩ ∈ 𝐶))
Theorem	resieq 4956	A restricted identity relation is equivalent to equality in its domain. (Contributed by NM, 30-Apr-2004.)
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵( I ↾ 𝐴)𝐶 ↔ 𝐵 = 𝐶))
Theorem	opelresi 4957	⟨𝐴, 𝐴⟩ belongs to a restriction of the identity class iff 𝐴 belongs to the restricting class. (Contributed by FL, 27-Oct-2008.) (Revised by NM, 30-Mar-2016.)
⊢ (𝐴 ∈ 𝑉 → (⟨𝐴, 𝐴⟩ ∈ ( I ↾ 𝐵) ↔ 𝐴 ∈ 𝐵))
Theorem	resres 4958	The restriction of a restriction. (Contributed by NM, 27-Mar-2008.)
⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ (𝐵 ∩ 𝐶))
Theorem	resundi 4959	Distributive law for restriction over union. Theorem 31 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.)
⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))
Theorem	resundir 4960	Distributive law for restriction over union. (Contributed by NM, 23-Sep-2004.)
⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶))
Theorem	resindi 4961	Class restriction distributes over intersection. (Contributed by FL, 6-Oct-2008.)
⊢ (𝐴 ↾ (𝐵 ∩ 𝐶)) = ((𝐴 ↾ 𝐵) ∩ (𝐴 ↾ 𝐶))
Theorem	resindir 4962	Class restriction distributes over intersection. (Contributed by NM, 18-Dec-2008.)
⊢ ((𝐴 ∩ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∩ (𝐵 ↾ 𝐶))
Theorem	inres 4963	Move intersection into class restriction. (Contributed by NM, 18-Dec-2008.)
⊢ (𝐴 ∩ (𝐵 ↾ 𝐶)) = ((𝐴 ∩ 𝐵) ↾ 𝐶)
Theorem	resdifcom 4964	Commutative law for restriction and difference. (Contributed by AV, 7-Jun-2021.)
⊢ ((𝐴 ↾ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ↾ 𝐵)
Theorem	resiun1 4965*	Distribution of restriction over indexed union. (Contributed by Mario Carneiro, 29-May-2015.)
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ↾ 𝐶) = ∪ 𝑥 ∈ 𝐴 (𝐵 ↾ 𝐶)
Theorem	resiun2 4966*	Distribution of restriction over indexed union. (Contributed by Mario Carneiro, 29-May-2015.)
⊢ (𝐶 ↾ ∪ 𝑥 ∈ 𝐴 𝐵) = ∪ 𝑥 ∈ 𝐴 (𝐶 ↾ 𝐵)
Theorem	dmres 4967	The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25. (Contributed by NM, 1-Aug-1994.)
⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)
Theorem	ssdmres 4968	A domain restricted to a subclass equals the subclass. (Contributed by NM, 2-Mar-1997.)
⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴)
Theorem	dmresexg 4969	The domain of a restriction to a set exists. (Contributed by NM, 7-Apr-1995.)
⊢ (𝐵 ∈ 𝑉 → dom (𝐴 ↾ 𝐵) ∈ V)
Theorem	resss 4970	A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.)
⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴
Theorem	rescom 4971	Commutative law for restriction. (Contributed by NM, 27-Mar-1998.)
⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ↾ 𝐵)
Theorem	ssres 4972	Subclass theorem for restriction. (Contributed by NM, 16-Aug-1994.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ↾ 𝐶) ⊆ (𝐵 ↾ 𝐶))
Theorem	ssres2 4973	Subclass theorem for restriction. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵))
Theorem	relres 4974	A restriction is a relation. Exercise 12 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ Rel (𝐴 ↾ 𝐵)
Theorem	resabs1 4975	Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25. (Contributed by NM, 9-Aug-1994.)
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))
Theorem	resabs1d 4976	Absorption law for restriction, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))
Theorem	resabs2 4977	Absorption law for restriction. (Contributed by NM, 27-Mar-1998.)
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ 𝐵))
Theorem	residm 4978	Idempotent law for restriction. (Contributed by NM, 27-Mar-1998.)
⊢ ((𝐴 ↾ 𝐵) ↾ 𝐵) = (𝐴 ↾ 𝐵)
Theorem	resima 4979	A restriction to an image. (Contributed by NM, 29-Sep-2004.)
⊢ ((𝐴 ↾ 𝐵) “ 𝐵) = (𝐴 “ 𝐵)
Theorem	resima2 4980	Image under a restricted class. (Contributed by FL, 31-Aug-2009.)
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) “ 𝐵) = (𝐴 “ 𝐵))
Theorem	xpssres 4981	Restriction of a constant function (or other cross product). (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐶 ⊆ 𝐴 → ((𝐴 × 𝐵) ↾ 𝐶) = (𝐶 × 𝐵))
Theorem	elres 4982*	Membership in a restriction. (Contributed by Scott Fenton, 17-Mar-2011.)
⊢ (𝐴 ∈ (𝐵 ↾ 𝐶) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐵))
Theorem	elsnres 4983*	Memebership in restriction to a singleton. (Contributed by Scott Fenton, 17-Mar-2011.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 ↾ {𝐶}) ↔ ∃𝑦(𝐴 = ⟨𝐶, 𝑦⟩ ∧ ⟨𝐶, 𝑦⟩ ∈ 𝐵))
Theorem	relssres 4984	Simplification law for restriction. (Contributed by NM, 16-Aug-1994.)
⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → (𝐴 ↾ 𝐵) = 𝐴)
Theorem	resdm 4985	A relation restricted to its domain equals itself. (Contributed by NM, 12-Dec-2006.)
⊢ (Rel 𝐴 → (𝐴 ↾ dom 𝐴) = 𝐴)
Theorem	resexg 4986	The restriction of a set is a set. (Contributed by NM, 28-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ 𝐵) ∈ V)
Theorem	resex 4987	The restriction of a set is a set. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ↾ 𝐵) ∈ V
Theorem	resindm 4988	When restricting a relation, intersecting with the domain of the relation has no effect. (Contributed by FL, 6-Oct-2008.)
⊢ (Rel 𝐴 → (𝐴 ↾ (𝐵 ∩ dom 𝐴)) = (𝐴 ↾ 𝐵))
Theorem	resdmdfsn 4989	Restricting a relation to its domain without a set is the same as restricting the relation to the universe without this set. (Contributed by AV, 2-Dec-2018.)
⊢ (Rel 𝑅 → (𝑅 ↾ (V ∖ {𝑋})) = (𝑅 ↾ (dom 𝑅 ∖ {𝑋})))
Theorem	resopab 4990*	Restriction of a class abstraction of ordered pairs. (Contributed by NM, 5-Nov-2002.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
Theorem	resiexg 4991	The existence of a restricted identity function, proved without using the Axiom of Replacement. (Contributed by NM, 13-Jan-2007.)
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V)
Theorem	iss 4992	A subclass of the identity function is the identity function restricted to its domain. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ⊆ I ↔ 𝐴 = ( I ↾ dom 𝐴))
Theorem	resopab2 4993*	Restriction of a class abstraction of ordered pairs. (Contributed by NM, 24-Aug-2007.)
⊢ (𝐴 ⊆ 𝐵 → ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
Theorem	resmpt 4994*	Restriction of the mapping operation. (Contributed by Mario Carneiro, 15-Jul-2013.)
⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	resmpt3 4995*	Unconditional restriction of the mapping operation. (Contributed by Stefan O'Rear, 24-Jan-2015.) (Proof shortened by Mario Carneiro, 22-Mar-2015.)
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ (𝐴 ∩ 𝐵) ↦ 𝐶)
Theorem	resmptf 4996	Restriction of the mapping operation. (Contributed by Thierry Arnoux, 28-Mar-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	resmptd 4997*	Restriction of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	dfres2 4998*	Alternate definition of the restriction operation. (Contributed by Mario Carneiro, 5-Nov-2013.)
⊢ (𝑅 ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥𝑅𝑦)}
Theorem	opabresid 4999*	The restricted identity relation expressed as an ordered-pair class abstraction. (Contributed by FL, 25-Apr-2012.)
⊢ ( I ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)}
Theorem	mptresid 5000*	The restricted identity relation expressed in maps-to notation. (Contributed by FL, 25-Apr-2012.)
⊢ ( I ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝑥)