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	resiun1 6001*	Distribution of restriction over indexed union. (Contributed by Mario Carneiro, 29-May-2015.) (Proof shortened by JJ, 25-Aug-2021.)
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ↾ 𝐶) = ∪ 𝑥 ∈ 𝐴 (𝐵 ↾ 𝐶)
Theorem	resiun2 6002*	Distribution of restriction over indexed union. (Contributed by Mario Carneiro, 29-May-2015.)
⊢ (𝐶 ↾ ∪ 𝑥 ∈ 𝐴 𝐵) = ∪ 𝑥 ∈ 𝐴 (𝐶 ↾ 𝐵)
Theorem	dmres 6003	The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25. (Contributed by NM, 1-Aug-1994.)
⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)
Theorem	ssdmres 6004	A domain restricted to a subclass equals the subclass. (Contributed by NM, 2-Mar-1997.)
⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴)
Theorem	dmresexg 6005	The domain of a restriction to a set exists. (Contributed by NM, 7-Apr-1995.)
⊢ (𝐵 ∈ 𝑉 → dom (𝐴 ↾ 𝐵) ∈ V)
Theorem	resss 6006	A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.)
⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴
Theorem	rescom 6007	Commutative law for restriction. (Contributed by NM, 27-Mar-1998.)
⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ↾ 𝐵)
Theorem	ssres 6008	Subclass theorem for restriction. (Contributed by NM, 16-Aug-1994.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ↾ 𝐶) ⊆ (𝐵 ↾ 𝐶))
Theorem	ssres2 6009	Subclass theorem for restriction. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵))
Theorem	relres 6010	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 6011	Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25. (Contributed by NM, 9-Aug-1994.)
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))
Theorem	resabs1d 6012	Absorption law for restriction, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))
Theorem	resabs2 6013	Absorption law for restriction. (Contributed by NM, 27-Mar-1998.)
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ 𝐵))
Theorem	residm 6014	Idempotent law for restriction. (Contributed by NM, 27-Mar-1998.)
⊢ ((𝐴 ↾ 𝐵) ↾ 𝐵) = (𝐴 ↾ 𝐵)
Theorem	resima 6015	A restriction to an image. (Contributed by NM, 29-Sep-2004.)
⊢ ((𝐴 ↾ 𝐵) “ 𝐵) = (𝐴 “ 𝐵)
Theorem	resima2 6016	Image under a restricted class. (Contributed by FL, 31-Aug-2009.) (Proof shortened by JJ, 25-Aug-2021.)
⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) “ 𝐵) = (𝐴 “ 𝐵))
Theorem	rnresss 6017	The range of a restriction is a subset of the whole range. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ran (𝐴 ↾ 𝐵) ⊆ ran 𝐴
Theorem	xpssres 6018	Restriction of a constant function (or other Cartesian product). (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐶 ⊆ 𝐴 → ((𝐴 × 𝐵) ↾ 𝐶) = (𝐶 × 𝐵))
Theorem	elinxp 6019*	Membership in an intersection with a Cartesian product. (Contributed by Peter Mazsa, 9-Sep-2022.)
⊢ (𝐶 ∈ (𝑅 ∩ (𝐴 × 𝐵)) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝐶 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑅))
Theorem	elres 6020*	Membership in a restriction. (Contributed by Scott Fenton, 17-Mar-2011.) (Proof shortened by Peter Mazsa, 9-Sep-2022.)
⊢ (𝐴 ∈ (𝐵 ↾ 𝐶) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐵))
Theorem	elsnres 6021*	Membership in restriction to a singleton. (Contributed by Scott Fenton, 17-Mar-2011.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 ↾ {𝐶}) ↔ ∃𝑦(𝐴 = ⟨𝐶, 𝑦⟩ ∧ ⟨𝐶, 𝑦⟩ ∈ 𝐵))
Theorem	relssres 6022	Simplification law for restriction. (Contributed by NM, 16-Aug-1994.)
⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵) → (𝐴 ↾ 𝐵) = 𝐴)
Theorem	dmressnsn 6023	The domain of a restriction to a singleton is a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ (𝐴 ∈ dom 𝐹 → dom (𝐹 ↾ {𝐴}) = {𝐴})
Theorem	eldmressnsn 6024	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 6025	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 6026	A relation restricted to its domain equals itself. (Contributed by NM, 12-Dec-2006.)
⊢ (Rel 𝐴 → (𝐴 ↾ dom 𝐴) = 𝐴)
Theorem	resexg 6027	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 6028	The restriction of a set is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 ↾ 𝐵) ∈ V)
Theorem	resex 6029	The restriction of a set is a set. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ↾ 𝐵) ∈ V
Theorem	resindm 6030	When restricting a relation, intersecting with the domain of the relation has no effect. (Contributed by FL, 6-Oct-2008.)
⊢ (Rel 𝐴 → (𝐴 ↾ (𝐵 ∩ dom 𝐴)) = (𝐴 ↾ 𝐵))
Theorem	resdmdfsn 6031	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 6032	Split a relation into two disjoint parts based on its domain. (Contributed by Thierry Arnoux, 9-Oct-2023.)
⊢ ((Rel 𝑅 ∧ dom 𝑅 = (𝐴 ∪ 𝐵) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝑅 = ((𝑅 ↾ 𝐴) ∪ (𝑅 ↾ 𝐵)))
Theorem	relresdm1 6033	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 6034*	Restriction of a class abstraction of ordered pairs. (Contributed by NM, 5-Nov-2002.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
Theorem	iss 6035	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 6036*	Restriction of a class abstraction of ordered pairs. (Contributed by NM, 24-Aug-2007.)
⊢ (𝐴 ⊆ 𝐵 → ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
Theorem	resmpt 6037*	Restriction of the mapping operation. (Contributed by Mario Carneiro, 15-Jul-2013.)
⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	resmpt3 6038*	Unconditional restriction of the mapping operation. (Contributed by Stefan O'Rear, 24-Jan-2015.) (Proof shortened by Mario Carneiro, 22-Mar-2015.)
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ (𝐴 ∩ 𝐵) ↦ 𝐶)
Theorem	resmptf 6039	Restriction of the mapping operation. (Contributed by Thierry Arnoux, 28-Mar-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	resmptd 6040*	Restriction of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	dfres2 6041*	Alternate definition of the restriction operation. (Contributed by Mario Carneiro, 5-Nov-2013.)
⊢ (𝑅 ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥𝑅𝑦)}
Theorem	mptss 6042*	Sufficient condition for inclusion among two functions in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⊆ (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	elidinxp 6043*	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 6044*	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 6045*	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 6046	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 6047) to cartesian product. (Revised by BJ, 23-Dec-2023.)
⊢ ( I ∩ (𝐴 × 𝐵)) = ( I ↾ (𝐴 ∩ 𝐵))
Theorem	idinxpresid 6047	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 6048	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 6049*	The restricted identity relation expressed as an ordered-pair class abstraction. (Contributed by FL, 25-Apr-2012.)
⊢ ( I ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)}
Theorem	mptresid 6050*	The restricted identity relation expressed in maps-to notation. (Contributed by FL, 25-Apr-2012.)
⊢ ( I ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝑥)
Theorem	dmresi 6051	The domain of a restricted identity function. (Contributed by NM, 27-Aug-2004.)
⊢ dom ( I ↾ 𝐴) = 𝐴
Theorem	restidsing 6052	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 6053	The identity function restricted to a class 𝐴 is empty iff the class 𝐴 is empty. (Contributed by AV, 30-Jan-2024.)
⊢ (𝐴 = ∅ ↔ ( I ↾ 𝐴) = ∅)
Theorem	imaeq1 6054	Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
Theorem	imaeq2 6055	Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
Theorem	imaeq1i 6056	Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶)
Theorem	imaeq2i 6057	Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵)
Theorem	imaeq1d 6058	Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
Theorem	imaeq2d 6059	Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
Theorem	imaeq12d 6060	Equality theorem for image. (Contributed by Mario Carneiro, 4-Dec-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐷))
Theorem	dfima2 6061*	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 6062*	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 6063*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 20-Jan-2007.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥 ∈ 𝐶 𝑥𝐵𝐴))
Theorem	elima 6064*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 19-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥 ∈ 𝐶 𝑥𝐵𝐴)
Theorem	elima2 6065*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 11-Aug-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ 𝑥𝐵𝐴))
Theorem	elima3 6066*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 14-Aug-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ ⟨𝑥, 𝐴⟩ ∈ 𝐵))
Theorem	nfima 6067	Bound-variable hypothesis builder for image. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 “ 𝐵)
Theorem	nfimad 6068	Deduction version of bound-variable hypothesis builder nfima 6067. (Contributed by FL, 15-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝐴 “ 𝐵))
Theorem	imadmrn 6069	The image of the domain of a class is the range of the class. (Contributed by NM, 14-Aug-1994.)
⊢ (𝐴 “ dom 𝐴) = ran 𝐴
Theorem	imassrn 6070	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 6071*	Image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐶) = ran (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ 𝐵)
Theorem	mptimass 6072*	Image of a function in maps-to notation for a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐶) = ran (𝑥 ∈ 𝐶 ↦ 𝐵))
Theorem	imai 6073	Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38. (Contributed by NM, 30-Apr-1998.)
⊢ ( I “ 𝐴) = 𝐴
Theorem	rnresi 6074	The range of the restricted identity function. (Contributed by NM, 27-Aug-2004.)
⊢ ran ( I ↾ 𝐴) = 𝐴
Theorem	resiima 6075	The image of a restriction of the identity function. (Contributed by FL, 31-Dec-2006.)
⊢ (𝐵 ⊆ 𝐴 → (( I ↾ 𝐴) “ 𝐵) = 𝐵)
Theorem	ima0 6076	Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by NM, 20-May-1998.)
⊢ (𝐴 “ ∅) = ∅
Theorem	0ima 6077	Image under the empty relation. (Contributed by FL, 11-Jan-2007.)
⊢ (∅ “ 𝐴) = ∅
Theorem	csbima12 6078	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 6079	A class whose image under another is empty is disjoint with the other's domain. (Contributed by FL, 24-Jan-2007.)
⊢ ((𝐴 “ 𝐵) = ∅ ↔ (dom 𝐴 ∩ 𝐵) = ∅)
Theorem	cnvimass 6080	A preimage under any class is included in the domain of the class. (Contributed by FL, 29-Jan-2007.)
⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴
Theorem	cnvimarndm 6081	The preimage of the range of a class is the domain of the class. (Contributed by Jeff Hankins, 15-Jul-2009.)
⊢ (◡𝐴 “ ran 𝐴) = dom 𝐴
Theorem	imasng 6082*	The image of a singleton. (Contributed by NM, 8-May-2005.)
⊢ (𝐴 ∈ 𝐵 → (𝑅 “ {𝐴}) = {𝑦 ∣ 𝐴𝑅𝑦})
Theorem	relimasn 6083*	The image of a singleton. (Contributed by NM, 20-May-1998.)
⊢ (Rel 𝑅 → (𝑅 “ {𝐴}) = {𝑦 ∣ 𝐴𝑅𝑦})
Theorem	elrelimasn 6084	Elementhood in the image of a singleton. (Contributed by Mario Carneiro, 3-Nov-2015.)
⊢ (Rel 𝑅 → (𝐵 ∈ (𝑅 “ {𝐴}) ↔ 𝐴𝑅𝐵))
Theorem	elimasng1 6085	Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006.) Revise to use df-br 5149 and to prove elimasn1 6086 from it. (Revised by BJ, 16-Oct-2024.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ 𝐵𝐴𝐶))
Theorem	elimasn1 6086	Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Use df-br 5149 and shorten proof. (Revised by BJ, 16-Oct-2024.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐶 ∈ (𝐴 “ {𝐵}) ↔ 𝐵𝐴𝐶)
Theorem	elimasng 6087	Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006.) TODO: replace existing usages by usages of elimasng1 6085, remove, and relabel elimasng1 6085 to "elimasng".
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴))
Theorem	elimasn 6088	Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by BJ, 16-Oct-2024.) TODO: replace existing usages by usages of elimasn1 6086, remove, and relabel elimasn1 6086 to "elimasn".
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)
Theorem	elimasngOLD 6089	Obsolete version of elimasng 6087 as of 16-Oct-2024. (Contributed by Raph Levien, 21-Oct-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴))
Theorem	elimasni 6090	Membership in an image of a singleton. (Contributed by NM, 5-Aug-2010.)
⊢ (𝐶 ∈ (𝐴 “ {𝐵}) → 𝐵𝐴𝐶)
Theorem	args 6091*	Two ways to express the class of unique-valued arguments of 𝐹, which is the same as the domain of 𝐹 whenever 𝐹 is a function. The left-hand side of the equality is from Definition 10.2 of [Quine] p. 65. Quine uses the notation "arg 𝐹 " for this class (for which we have no separate notation). Observe the resemblance to the alternate definition dffv4 6888 of function value, which is based on the idea in Quine's definition. (Contributed by NM, 8-May-2005.)
⊢ {𝑥 ∣ ∃𝑦(𝐹 “ {𝑥}) = {𝑦}} = {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦}
Theorem	elinisegg 6092	Membership in the inverse image of a singleton. (Contributed by NM, 28-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Put in closed form and shorten proof. (Revised by BJ, 16-Oct-2024.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵))
Theorem	eliniseg 6093	Membership in the inverse image of a singleton. An application is to express initial segments for an order relation. See for example Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 28-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐵 ∈ 𝑉 → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵))
Theorem	epin 6094	Any set is equal to its preimage under the converse membership relation. (Contributed by Mario Carneiro, 9-Mar-2013.) Put in closed form. (Revised by BJ, 16-Oct-2024.)
⊢ (𝐴 ∈ 𝑉 → (◡ E “ {𝐴}) = 𝐴)
Theorem	epini 6095	Any set is equal to its preimage under the converse membership relation. (Contributed by Mario Carneiro, 9-Mar-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (◡ E “ {𝐴}) = 𝐴
Theorem	iniseg 6096*	An idiom that signifies an initial segment of an ordering, used, for example, in Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 28-Apr-2004.)
⊢ (𝐵 ∈ 𝑉 → (◡𝐴 “ {𝐵}) = {𝑥 ∣ 𝑥𝐴𝐵})
Theorem	inisegn0 6097	Nonemptiness of an initial segment in terms of range. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ (𝐴 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝐴}) ≠ ∅)
Theorem	dffr3 6098*	Alternate definition of well-founded relation. Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 23-Apr-2004.) (Revised by Mario Carneiro, 23-Jun-2015.)
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅))
Theorem	dfse2 6099*	Alternate definition of set-like relation. (Contributed by Mario Carneiro, 23-Jun-2015.)
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 (𝐴 ∩ (◡𝑅 “ {𝑥})) ∈ V)
Theorem	imass1 6100	Subset theorem for image. (Contributed by NM, 16-Mar-2004.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 “ 𝐶) ⊆ (𝐵 “ 𝐶))