P. 61 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6001-6100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nfres 6001	Bound-variable hypothesis builder for restriction. (Contributed by NM, 15-Sep-2003.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)
Theorem	csbres 6002	Distribute proper substitution through the restriction of a class. (Contributed by Alan Sare, 10-Nov-2012.) (Revised by NM, 23-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶)
Theorem	res0 6003	A restriction to the empty set is empty. (Contributed by NM, 12-Nov-1994.)
⊢ (𝐴 ↾ ∅) = ∅
Theorem	dfres3 6004	Alternate definition of restriction. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × ran 𝐴))
Theorem	opelres 6005	Ordered pair elementhood in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by NM, 13-Nov-1995.) (Revised by BJ, 18-Feb-2022.) Commute the consequent. (Revised by Peter Mazsa, 24-Sep-2022.)
⊢ (𝐶 ∈ 𝑉 → (⟨𝐵, 𝐶⟩ ∈ (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ ⟨𝐵, 𝐶⟩ ∈ 𝑅)))
Theorem	brres 6006	Binary relation on a restriction. (Contributed by Mario Carneiro, 4-Nov-2015.) Commute the consequent. (Revised by Peter Mazsa, 24-Sep-2022.)
⊢ (𝐶 ∈ 𝑉 → (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶)))
Theorem	opelresi 6007	Ordered pair membership in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by NM, 13-Nov-1995.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐵, 𝐶⟩ ∈ (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
Theorem	brresi 6008	Binary relation on a restriction. (Contributed by NM, 12-Dec-2006.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶))
Theorem	opres 6009	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 6010	A restricted identity relation is equivalent to equality in its domain. (Contributed by NM, 30-Apr-2004.)
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵( I ↾ 𝐴)𝐶 ↔ 𝐵 = 𝐶))
Theorem	opelidres 6011	⟨𝐴, 𝐴⟩ 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 6012	The restriction of a restriction. (Contributed by NM, 27-Mar-2008.)
⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ (𝐵 ∩ 𝐶))
Theorem	resundi 6013	Distributive law for restriction over union. Theorem 31 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.)
⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))
Theorem	resundir 6014	Distributive law for restriction over union. (Contributed by NM, 23-Sep-2004.)
⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶))
Theorem	resindi 6015	Class restriction distributes over intersection. (Contributed by FL, 6-Oct-2008.)
⊢ (𝐴 ↾ (𝐵 ∩ 𝐶)) = ((𝐴 ↾ 𝐵) ∩ (𝐴 ↾ 𝐶))
Theorem	resindir 6016	Class restriction distributes over intersection. (Contributed by NM, 18-Dec-2008.)
⊢ ((𝐴 ∩ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∩ (𝐵 ↾ 𝐶))
Theorem	inres 6017	Move intersection into class restriction. (Contributed by NM, 18-Dec-2008.)
⊢ (𝐴 ∩ (𝐵 ↾ 𝐶)) = ((𝐴 ∩ 𝐵) ↾ 𝐶)
Theorem	resdifcom 6018	Commutative law for restriction and difference. (Contributed by AV, 7-Jun-2021.)
⊢ ((𝐴 ↾ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ↾ 𝐵)
Theorem	resiun1 6019*	Distribution of restriction over indexed union. (Contributed by Mario Carneiro, 29-May-2015.) (Proof shortened by JJ, 25-Aug-2021.)
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ↾ 𝐶) = ∪ 𝑥 ∈ 𝐴 (𝐵 ↾ 𝐶)
Theorem	resiun2 6020*	Distribution of restriction over indexed union. (Contributed by Mario Carneiro, 29-May-2015.)
⊢ (𝐶 ↾ ∪ 𝑥 ∈ 𝐴 𝐵) = ∪ 𝑥 ∈ 𝐴 (𝐶 ↾ 𝐵)
Theorem	resss 6021	A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.)
⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴
Theorem	rescom 6022	Commutative law for restriction. (Contributed by NM, 27-Mar-1998.)
⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ↾ 𝐵)
Theorem	ssres 6023	Subclass theorem for restriction. (Contributed by NM, 16-Aug-1994.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ↾ 𝐶) ⊆ (𝐵 ↾ 𝐶))
Theorem	ssres2 6024	Subclass theorem for restriction. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵))
Theorem	relres 6025	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 6026	Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25. (Contributed by NM, 9-Aug-1994.)
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))
Theorem	resabs1d 6027	Absorption law for restriction, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))
Theorem	resabs2 6028	Absorption law for restriction. (Contributed by NM, 27-Mar-1998.)
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ 𝐵))
Theorem	residm 6029	Idempotent law for restriction. (Contributed by NM, 27-Mar-1998.)
⊢ ((𝐴 ↾ 𝐵) ↾ 𝐵) = (𝐴 ↾ 𝐵)
Theorem	dmresss 6030	The domain of a restriction is a subset of the original domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) Proof shortened and axiom usage reduced. (Proof shortened by AV, 15-May-2025.)
⊢ dom (𝐴 ↾ 𝐵) ⊆ dom 𝐴
Theorem	dmres 6031	The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25. (Contributed by NM, 1-Aug-1994.)
⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)
Theorem	ssdmres 6032	A domain restricted to a subclass equals the subclass. (Contributed by NM, 2-Mar-1997.)
⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴)
Theorem	dmresexg 6033	The domain of a restriction to a set exists. (Contributed by NM, 7-Apr-1995.)
⊢ (𝐵 ∈ 𝑉 → dom (𝐴 ↾ 𝐵) ∈ V)
Theorem	resima 6034	A restriction to an image. (Contributed by NM, 29-Sep-2004.)
⊢ ((𝐴 ↾ 𝐵) “ 𝐵) = (𝐴 “ 𝐵)
Theorem	resima2 6035	Image under a restricted class. (Contributed by FL, 31-Aug-2009.) (Proof shortened by JJ, 25-Aug-2021.)
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) “ 𝐵) = (𝐴 “ 𝐵))
Theorem	rnresss 6036	The range of a restriction is a subset of the whole range. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ran (𝐴 ↾ 𝐵) ⊆ ran 𝐴
Theorem	xpssres 6037	Restriction of a constant function (or other Cartesian product). (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐶 ⊆ 𝐴 → ((𝐴 × 𝐵) ↾ 𝐶) = (𝐶 × 𝐵))
Theorem	elinxp 6038*	Membership in an intersection with a Cartesian product. (Contributed by Peter Mazsa, 9-Sep-2022.)
⊢ (𝐶 ∈ (𝑅 ∩ (𝐴 × 𝐵)) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝐶 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑅))
Theorem	elres 6039*	Membership in a restriction. (Contributed by Scott Fenton, 17-Mar-2011.) (Proof shortened by Peter Mazsa, 9-Sep-2022.)
⊢ (𝐴 ∈ (𝐵 ↾ 𝐶) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐵))
Theorem	elsnres 6040*	Membership in restriction to a singleton. (Contributed by Scott Fenton, 17-Mar-2011.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 ↾ {𝐶}) ↔ ∃𝑦(𝐴 = ⟨𝐶, 𝑦⟩ ∧ ⟨𝐶, 𝑦⟩ ∈ 𝐵))
Theorem	relssres 6041	Simplification law for restriction. (Contributed by NM, 16-Aug-1994.)
⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → (𝐴 ↾ 𝐵) = 𝐴)
Theorem	dmressnsn 6042	The domain of a restriction to a singleton is a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ (𝐴 ∈ dom 𝐹 → dom (𝐹 ↾ {𝐴}) = {𝐴})
Theorem	eldmressnsn 6043	The element of the domain of a restriction to a singleton is the element of the singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ (𝐴 ∈ dom 𝐹 → 𝐴 ∈ dom (𝐹 ↾ {𝐴}))
Theorem	eldmeldmressn 6044	An element of the domain (of a relation) is an element of the domain of the restriction (of the relation) to the singleton containing this element. (Contributed by Alexander van der Vekens, 22-Jul-2018.)
⊢ (𝑋 ∈ dom 𝐹 ↔ 𝑋 ∈ dom (𝐹 ↾ {𝑋}))
Theorem	resdm 6045	A relation restricted to its domain equals itself. (Contributed by NM, 12-Dec-2006.)
⊢ (Rel 𝐴 → (𝐴 ↾ dom 𝐴) = 𝐴)
Theorem	resexg 6046	The restriction of a set is a set. (Contributed by NM, 28-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↾ 𝐵) ∈ V)
Theorem	resexd 6047	The restriction of a set is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 ↾ 𝐵) ∈ V)
Theorem	resex 6048	The restriction of a set is a set. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ↾ 𝐵) ∈ V
Theorem	resindm 6049	When restricting a relation, intersecting with the domain of the relation has no effect. (Contributed by FL, 6-Oct-2008.)
⊢ (Rel 𝐴 → (𝐴 ↾ (𝐵 ∩ dom 𝐴)) = (𝐴 ↾ 𝐵))
Theorem	resdmdfsn 6050	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	reldisjun 6051	Split a relation into two disjoint parts based on its domain. (Contributed by Thierry Arnoux, 9-Oct-2023.)
⊢ ((Rel 𝑅 ∧ dom 𝑅 = (𝐴 ∪ 𝐵) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝑅 = ((𝑅 ↾ 𝐴) ∪ (𝑅 ↾ 𝐵)))
Theorem	relresdm1 6052	Restriction of a disjoint union to the domain of the first term. (Contributed by Thierry Arnoux, 9-Dec-2021.)
⊢ ((Rel 𝐴 ∧ (dom 𝐴 ∩ dom 𝐵) = ∅) → ((𝐴 ∪ 𝐵) ↾ dom 𝐴) = 𝐴)
Theorem	resopab 6053*	Restriction of a class abstraction of ordered pairs. (Contributed by NM, 5-Nov-2002.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
Theorem	iss 6054	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 6055*	Restriction of a class abstraction of ordered pairs. (Contributed by NM, 24-Aug-2007.)
⊢ (𝐴 ⊆ 𝐵 → ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
Theorem	resmpt 6056*	Restriction of the mapping operation. (Contributed by Mario Carneiro, 15-Jul-2013.)
⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	resmpt3 6057*	Unconditional restriction of the mapping operation. (Contributed by Stefan O'Rear, 24-Jan-2015.) (Proof shortened by Mario Carneiro, 22-Mar-2015.)
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ (𝐴 ∩ 𝐵) ↦ 𝐶)
Theorem	resmptf 6058	Restriction of the mapping operation. (Contributed by Thierry Arnoux, 28-Mar-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	resmptd 6059*	Restriction of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	dfres2 6060*	Alternate definition of the restriction operation. (Contributed by Mario Carneiro, 5-Nov-2013.)
⊢ (𝑅 ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥𝑅𝑦)}
Theorem	mptss 6061*	Sufficient condition for inclusion among two functions in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⊆ (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	elimampt 6062*	Membership in the image of a mapping. (Contributed by Thierry Arnoux, 3-Jan-2022.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐹 “ 𝐷) ↔ ∃𝑥 ∈ 𝐷 𝐶 = 𝐵))
Theorem	elidinxp 6063*	Characterization of the elements of the intersection of the identity relation with a Cartesian product. (Contributed by Peter Mazsa, 9-Sep-2022.)
⊢ (𝐶 ∈ ( I ∩ (𝐴 × 𝐵)) ↔ ∃𝑥 ∈ (𝐴 ∩ 𝐵)𝐶 = ⟨𝑥, 𝑥⟩)
Theorem	elidinxpid 6064*	Characterization of the elements of the intersection of the identity relation with a Cartesian square. (Contributed by Peter Mazsa, 9-Sep-2022.)
⊢ (𝐵 ∈ ( I ∩ (𝐴 × 𝐴)) ↔ ∃𝑥 ∈ 𝐴 𝐵 = ⟨𝑥, 𝑥⟩)
Theorem	elrid 6065*	Characterization of the elements of a restricted identity relation. (Contributed by BJ, 28-Aug-2022.) (Proof shortened by Peter Mazsa, 9-Sep-2022.)
⊢ (𝐴 ∈ ( I ↾ 𝑋) ↔ ∃𝑥 ∈ 𝑋 𝐴 = ⟨𝑥, 𝑥⟩)
Theorem	idinxpres 6066	The intersection of the identity relation with a cartesian product is the restriction of the identity relation to the intersection of the factors. (Contributed by FL, 2-Aug-2009.) (Proof shortened by Peter Mazsa, 9-Sep-2022.) Generalize statement from cartesian square (now idinxpresid 6067) to cartesian product. (Revised by BJ, 23-Dec-2023.)
⊢ ( I ∩ (𝐴 × 𝐵)) = ( I ↾ (𝐴 ∩ 𝐵))
Theorem	idinxpresid 6067	The intersection of the identity relation with the cartesian square of a class is the restriction of the identity relation to that class. (Contributed by FL, 2-Aug-2009.) (Proof shortened by Peter Mazsa, 9-Sep-2022.) (Proof shortened by BJ, 23-Dec-2023.)
⊢ ( I ∩ (𝐴 × 𝐴)) = ( I ↾ 𝐴)
Theorem	idssxp 6068	A diagonal set as a subset of a Cartesian square. (Contributed by Thierry Arnoux, 29-Dec-2019.) (Proof shortened by BJ, 9-Sep-2022.)
⊢ ( I ↾ 𝐴) ⊆ (𝐴 × 𝐴)
Theorem	opabresid 6069*	The restricted identity relation expressed as an ordered-pair class abstraction. (Contributed by FL, 25-Apr-2012.)
⊢ ( I ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)}
Theorem	mptresid 6070*	The restricted identity relation expressed in maps-to notation. (Contributed by FL, 25-Apr-2012.)
⊢ ( I ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝑥)
Theorem	dmresi 6071	The domain of a restricted identity function. (Contributed by NM, 27-Aug-2004.)
⊢ dom ( I ↾ 𝐴) = 𝐴
Theorem	restidsing 6072	Restriction of the identity to a singleton. (Contributed by FL, 2-Aug-2009.) (Proof shortened by JJ, 25-Aug-2021.) (Proof shortened by Peter Mazsa, 6-Oct-2022.)
⊢ ( I ↾ {𝐴}) = ({𝐴} × {𝐴})
Theorem	iresn0n0 6073	The identity function restricted to a class 𝐴 is empty iff the class 𝐴 is empty. (Contributed by AV, 30-Jan-2024.)
⊢ (𝐴 = ∅ ↔ ( I ↾ 𝐴) = ∅)
Theorem	imaeq1 6074	Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
Theorem	imaeq2 6075	Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
Theorem	imaeq1i 6076	Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶)
Theorem	imaeq2i 6077	Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵)
Theorem	imaeq1d 6078	Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
Theorem	imaeq2d 6079	Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
Theorem	imaeq12d 6080	Equality theorem for image. (Contributed by Mario Carneiro, 4-Dec-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐷))
Theorem	dfima2 6081*	Alternate definition of image. Compare definition (d) of [Enderton] p. 44. (Contributed by NM, 19-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑥𝐴𝑦}
Theorem	dfima3 6082*	Alternate definition of image. Compare definition (d) of [Enderton] p. 44. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
Theorem	elimag 6083*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 20-Jan-2007.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥 ∈ 𝐶 𝑥𝐵𝐴))
Theorem	elima 6084*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 19-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥 ∈ 𝐶 𝑥𝐵𝐴)
Theorem	elima2 6085*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 11-Aug-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ 𝑥𝐵𝐴))
Theorem	elima3 6086*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 14-Aug-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ ⟨𝑥, 𝐴⟩ ∈ 𝐵))
Theorem	nfima 6087	Bound-variable hypothesis builder for image. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 “ 𝐵)
Theorem	nfimad 6088	Deduction version of bound-variable hypothesis builder nfima 6087. (Contributed by FL, 15-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝐴 “ 𝐵))
Theorem	imadmrn 6089	The image of the domain of a class is the range of the class. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 “ dom 𝐴) = ran 𝐴
Theorem	imassrn 6090	The image of a class is a subset of its range. Theorem 3.16(xi) of [Monk1] p. 39. (Contributed by NM, 31-Mar-1995.)
⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴
Theorem	mptima 6091*	Image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐶) = ran (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ 𝐵)
Theorem	mptimass 6092*	Image of a function in maps-to notation for a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐶) = ran (𝑥 ∈ 𝐶 ↦ 𝐵))
Theorem	imai 6093	Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38. (Contributed by NM, 30-Apr-1998.)
⊢ ( I “ 𝐴) = 𝐴
Theorem	rnresi 6094	The range of the restricted identity function. (Contributed by NM, 27-Aug-2004.)
⊢ ran ( I ↾ 𝐴) = 𝐴
Theorem	resiima 6095	The image of a restriction of the identity function. (Contributed by FL, 31-Dec-2006.)
⊢ (𝐵 ⊆ 𝐴 → (( I ↾ 𝐴) “ 𝐵) = 𝐵)
Theorem	ima0 6096	Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by NM, 20-May-1998.)
⊢ (𝐴 “ ∅) = ∅
Theorem	0ima 6097	Image under the empty relation. (Contributed by FL, 11-Jan-2007.)
⊢ (∅ “ 𝐴) = ∅
Theorem	csbima12 6098	Move class substitution in and out of the image of a function. (Contributed by FL, 15-Dec-2006.) (Revised by NM, 20-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵)
Theorem	imadisj 6099	A class whose image under another is empty is disjoint with the other's domain. (Contributed by FL, 24-Jan-2007.)
⊢ ((𝐴 “ 𝐵) = ∅ ↔ (dom 𝐴 ∩ 𝐵) = ∅)
Theorem	imadisjlnd 6100	Deduction form of one negated side of imadisj 6099. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → (dom 𝐴 ∩ 𝐵) ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐵) ≠ ∅)