P. 59 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 5801-5900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	difxp1 5801	Difference law for Cartesian product. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 26-Jun-2014.)
⊢ ((𝐴 ∖ 𝐵) × 𝐶) = ((𝐴 × 𝐶) ∖ (𝐵 × 𝐶))
Theorem	difxp2 5802	Difference law for Cartesian product. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 26-Jun-2014.)
⊢ (𝐴 × (𝐵 ∖ 𝐶)) = ((𝐴 × 𝐵) ∖ (𝐴 × 𝐶))
Theorem	djudisj 5803*	Disjoint unions with disjoint index sets are disjoint. (Contributed by Stefan O'Rear, 21-Nov-2014.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐶) ∩ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝐷)) = ∅)
Theorem	xpdifid 5804*	The set of distinct couples in a Cartesian product. (Contributed by Thierry Arnoux, 25-May-2019.)
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) = ((𝐴 × 𝐵) ∖ I )
Theorem	resdisj 5805	A double restriction to disjoint classes is the empty set. (Contributed by NM, 7-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 ↾ 𝐴) ↾ 𝐵) = ∅)
Theorem	rnxp 5806	The range of a Cartesian product. Part of Theorem 3.13(x) of [Monk1] p. 37. (Contributed by NM, 12-Apr-2004.)
⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)
Theorem	dmxpss 5807	The domain of a Cartesian product is a subclass of the first factor. (Contributed by NM, 19-Mar-2007.)
⊢ dom (𝐴 × 𝐵) ⊆ 𝐴
Theorem	rnxpss 5808	The range of a Cartesian product is a subclass of the second factor. (Contributed by NM, 16-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ran (𝐴 × 𝐵) ⊆ 𝐵
Theorem	rnxpid 5809	The range of a square Cartesian product. (Contributed by FL, 17-May-2010.)
⊢ ran (𝐴 × 𝐴) = 𝐴
Theorem	ssxpb 5810	A Cartesian product subclass relationship is equivalent to the relationship for it components. (Contributed by NM, 17-Dec-2008.)
⊢ ((𝐴 × 𝐵) ≠ ∅ → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷)))
Theorem	xp11 5811	The Cartesian product of nonempty classes is one-to-one. (Contributed by NM, 31-May-2008.)
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((𝐴 × 𝐵) = (𝐶 × 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	xpcan 5812	Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.)
⊢ (𝐶 ≠ ∅ → ((𝐶 × 𝐴) = (𝐶 × 𝐵) ↔ 𝐴 = 𝐵))
Theorem	xpcan2 5813	Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.)
⊢ (𝐶 ≠ ∅ → ((𝐴 × 𝐶) = (𝐵 × 𝐶) ↔ 𝐴 = 𝐵))
Theorem	ssrnres 5814	Subset of the range of a restriction. (Contributed by NM, 16-Jan-2006.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) ↔ ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵)
Theorem	rninxp 5815*	Range of the intersection with a Cartesian product. (Contributed by NM, 17-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐶𝑦)
Theorem	dminxp 5816*	Domain of the intersection with a Cartesian product. (Contributed by NM, 17-Jan-2006.)
⊢ (dom (𝐶 ∩ (𝐴 × 𝐵)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥𝐶𝑦)
Theorem	imainrect 5817	Image of a relation restricted to a rectangular region. (Contributed by Stefan O'Rear, 19-Feb-2015.)
⊢ ((𝐺 ∩ (𝐴 × 𝐵)) “ 𝑌) = ((𝐺 “ (𝑌 ∩ 𝐴)) ∩ 𝐵)
Theorem	xpima 5818	The image by a constant function (or other Cartesian product). (Contributed by Thierry Arnoux, 4-Feb-2017.)
⊢ ((𝐴 × 𝐵) “ 𝐶) = if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵)
Theorem	xpima1 5819	The image by a Cartesian product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) “ 𝐶) = ∅)
Theorem	xpima2 5820	The image by a Cartesian product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
⊢ ((𝐴 ∩ 𝐶) ≠ ∅ → ((𝐴 × 𝐵) “ 𝐶) = 𝐵)
Theorem	xpimasn 5821	The image of a singleton by a Cartesian product. (Contributed by Thierry Arnoux, 14-Jan-2018.) (Proof shortened by BJ, 6-Apr-2019.)
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵)
Theorem	sossfld 5822	The base set of a strict order is contained in the field of the relation, except possibly for one element (note that ∅ Or {𝐵}). (Contributed by Mario Carneiro, 27-Apr-2015.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐴 ∖ {𝐵}) ⊆ (dom 𝑅 ∪ ran 𝑅))
Theorem	sofld 5823	The base set of a nonempty strict order is the same as the field of the relation. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴) ∧ 𝑅 ≠ ∅) → 𝐴 = (dom 𝑅 ∪ ran 𝑅))
Theorem	cnvcnv3 5824*	The set of all ordered pairs in a class is the same as the double converse. (Contributed by Mario Carneiro, 16-Aug-2015.)
⊢ ◡◡𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦}
Theorem	dfrel2 5825	Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.)
⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)
Theorem	dfrel4v 5826*	A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 6489 for relations. (Contributed by Mario Carneiro, 16-Aug-2015.)
⊢ (Rel 𝑅 ↔ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦})
Theorem	dfrel4 5827*	A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 6489 for relations. (Contributed by Mario Carneiro, 16-Aug-2015.) (Revised by Thierry Arnoux, 11-May-2017.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑦𝑅    ⇒   ⊢ (Rel 𝑅 ↔ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦})
Theorem	cnvcnv 5828	The double converse of a class strips out all elements that are not ordered pairs. (Contributed by NM, 8-Dec-2003.) (Proof shortened by BJ, 26-Nov-2021.)
⊢ ◡◡𝐴 = (𝐴 ∩ (V × V))
Theorem	cnvcnv2 5829	The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007.)
⊢ ◡◡𝐴 = (𝐴 ↾ V)
Theorem	cnvcnvss 5830	The double converse of a class is a subclass. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 23-Jul-2004.)
⊢ ◡◡𝐴 ⊆ 𝐴
Theorem	cnveqb 5831	Equality theorem for converse. (Contributed by FL, 19-Sep-2011.)
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ◡𝐴 = ◡𝐵))
Theorem	cnveq0 5832	A relation empty iff its converse is empty. (Contributed by FL, 19-Sep-2011.)
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ◡𝐴 = ∅))
Theorem	dfrel3 5833	Alternate definition of relation. (Contributed by NM, 14-May-2008.)
⊢ (Rel 𝑅 ↔ (𝑅 ↾ V) = 𝑅)
Theorem	elid 5834*	Characterization of the elements of the identity relation. TODO: reorder theorems to move this theorem and dfrel3 5833 after elrid 5695. (Contributed by BJ, 28-Aug-2022.)
⊢ (𝐴 ∈ I ↔ ∃𝑥 𝐴 = ⟨𝑥, 𝑥⟩)
Theorem	dmresv 5835	The domain of a universal restriction. (Contributed by NM, 14-May-2008.)
⊢ dom (𝐴 ↾ V) = dom 𝐴
Theorem	rnresv 5836	The range of a universal restriction. (Contributed by NM, 14-May-2008.)
⊢ ran (𝐴 ↾ V) = ran 𝐴
Theorem	dfrn4 5837	Range defined in terms of image. (Contributed by NM, 14-May-2008.)
⊢ ran 𝐴 = (𝐴 “ V)
Theorem	csbrn 5838	Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.)
⊢ ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵
Theorem	rescnvcnv 5839	The restriction of the double converse of a class. (Contributed by NM, 8-Apr-2007.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (◡◡𝐴 ↾ 𝐵) = (𝐴 ↾ 𝐵)
Theorem	cnvcnvres 5840	The double converse of the restriction of a class. (Contributed by NM, 3-Jun-2007.)
⊢ ◡◡(𝐴 ↾ 𝐵) = (◡◡𝐴 ↾ 𝐵)
Theorem	imacnvcnv 5841	The image of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
⊢ (◡◡𝐴 “ 𝐵) = (𝐴 “ 𝐵)
Theorem	dmsnn0 5842	The domain of a singleton is nonzero iff the singleton argument is an ordered pair. (Contributed by NM, 14-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ∈ (V × V) ↔ dom {𝐴} ≠ ∅)
Theorem	rnsnn0 5843	The range of a singleton is nonzero iff the singleton argument is an ordered pair. (Contributed by NM, 14-Dec-2008.)
⊢ (𝐴 ∈ (V × V) ↔ ran {𝐴} ≠ ∅)
Theorem	dmsn0 5844	The domain of the singleton of the empty set is empty. (Contributed by NM, 30-Jan-2004.)
⊢ dom {∅} = ∅
Theorem	cnvsn0 5845	The converse of the singleton of the empty set is empty. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ ◡{∅} = ∅
Theorem	dmsn0el 5846	The domain of a singleton is empty if the singleton's argument contains the empty set. (Contributed by NM, 15-Dec-2008.)
⊢ (∅ ∈ 𝐴 → dom {𝐴} = ∅)
Theorem	relsn2 5847	A singleton is a relation iff it has a nonempty domain. (Contributed by NM, 25-Sep-2013.) Make hypothesis an antecedent. (Revised by BJ, 12-Feb-2022.)
⊢ (𝐴 ∈ 𝑉 → (Rel {𝐴} ↔ dom {𝐴} ≠ ∅))
Theorem	dmsnopg 5848	The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐵 ∈ 𝑉 → dom {⟨𝐴, 𝐵⟩} = {𝐴})
Theorem	dmsnopss 5849	The domain of a singleton of an ordered pair is a subset of the singleton of the first member (with no sethood assumptions on 𝐵). (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ dom {⟨𝐴, 𝐵⟩} ⊆ {𝐴}
Theorem	dmpropg 5850	The domain of an unordered pair of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {𝐴, 𝐶})
Theorem	dmsnop 5851	The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by NM, 30-Jan-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐵 ∈ V    ⇒   ⊢ dom {⟨𝐴, 𝐵⟩} = {𝐴}
Theorem	dmprop 5852	The domain of an unordered pair of ordered pairs. (Contributed by NM, 13-Sep-2011.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {𝐴, 𝐶}
Theorem	dmtpop 5853	The domain of an unordered triple of ordered pairs. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩} = {𝐴, 𝐶, 𝐸}
Theorem	cnvcnvsn 5854	Double converse of a singleton of an ordered pair. (Unlike cnvsn 5861, this does not need any sethood assumptions on 𝐴 and 𝐵.) (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ◡◡{⟨𝐴, 𝐵⟩} = ◡{⟨𝐵, 𝐴⟩}
Theorem	dmsnsnsn 5855	The domain of the singleton of the singleton of a singleton. (Contributed by NM, 15-Sep-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ dom {{{𝐴}}} = {𝐴}
Theorem	rnsnopg 5856	The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → ran {⟨𝐴, 𝐵⟩} = {𝐵})
Theorem	rnpropg 5857	The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} = {𝐶, 𝐷})
Theorem	cnvsng 5858	Converse of a singleton of an ordered pair. (Contributed by NM, 23-Jan-2015.) (Proof shortened by BJ, 12-Feb-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{⟨𝐴, 𝐵⟩} = {⟨𝐵, 𝐴⟩})
Theorem	rnsnop 5859	The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ran {⟨𝐴, 𝐵⟩} = {𝐵}
Theorem	op1sta 5860	Extract the first member of an ordered pair. (See op2nda 5863 to extract the second member, op1stb 5161 for an alternate version, and op1st 7437 for the preferred version.) (Contributed by Raph Levien, 4-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ dom {⟨𝐴, 𝐵⟩} = 𝐴
Theorem	cnvsn 5861	Converse of a singleton of an ordered pair. (Contributed by NM, 11-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) (Proof shortened by BJ, 12-Feb-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ◡{⟨𝐴, 𝐵⟩} = {⟨𝐵, 𝐴⟩}
Theorem	op2ndb 5862	Extract the second member of an ordered pair. Theorem 5.12(ii) of [Monk1] p. 52. (See op1stb 5161 to extract the first member, op2nda 5863 for an alternate version, and op2nd 7438 for the preferred version.) (Contributed by NM, 25-Nov-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ ∩ ∩ ◡{⟨𝐴, 𝐵⟩} = 𝐵
Theorem	op2nda 5863	Extract the second member of an ordered pair. (See op1sta 5860 to extract the first member, op2ndb 5862 for an alternate version, and op2nd 7438 for the preferred version.) (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ ran {⟨𝐴, 𝐵⟩} = 𝐵
Theorem	opswap 5864	Swap the members of an ordered pair. (Contributed by NM, 14-Dec-2008.) (Revised by Mario Carneiro, 30-Aug-2015.)
⊢ ∪ ◡{⟨𝐴, 𝐵⟩} = ⟨𝐵, 𝐴⟩
Theorem	cnvresima 5865	An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.)
⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴)
Theorem	resdm2 5866	A class restricted to its domain equals its double converse. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 ↾ dom 𝐴) = ◡◡𝐴
Theorem	resdmres 5867	Restriction to the domain of a restriction. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 ↾ dom (𝐴 ↾ 𝐵)) = (𝐴 ↾ 𝐵)
Theorem	resresdm 5868	A restriction by an arbitrary set is a restriction by its domain. (Contributed by AV, 16-Nov-2020.)
⊢ (𝐹 = (𝐸 ↾ 𝐴) → 𝐹 = (𝐸 ↾ dom 𝐹))
Theorem	imadmres 5869	The image of the domain of a restriction. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 “ dom (𝐴 ↾ 𝐵)) = (𝐴 “ 𝐵)
Theorem	mptpreima 5870*	The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
Theorem	mptiniseg 5871*	Converse singleton image of a function defined by maps-to. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝐶 ∈ 𝑉 → (◡𝐹 “ {𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐵 = 𝐶})
Theorem	dmmpt 5872	The domain of the mapping operation in general. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 22-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
Theorem	dmmptss 5873*	The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ dom 𝐹 ⊆ 𝐴
Theorem	dmmptg 5874*	The domain of the mapping operation is the stated domain, if the function value is always a set. (Contributed by Mario Carneiro, 9-Feb-2013.) (Revised by Mario Carneiro, 14-Sep-2013.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)
Theorem	relco 5875	A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.)
⊢ Rel (𝐴 ∘ 𝐵)
Theorem	dfco2 5876*	Alternate definition of a class composition, using only one bound variable. (Contributed by NM, 19-Dec-2008.)
⊢ (𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))
Theorem	dfco2a 5877*	Generalization of dfco2 5876, where 𝐶 can have any value between dom 𝐴 ∩ ran 𝐵 and V. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((dom 𝐴 ∩ ran 𝐵) ⊆ 𝐶 → (𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ 𝐶 ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})))
Theorem	coundi 5878	Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶))
Theorem	coundir 5879	Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝐴 ∪ 𝐵) ∘ 𝐶) = ((𝐴 ∘ 𝐶) ∪ (𝐵 ∘ 𝐶))
Theorem	cores 5880	Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (ran 𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ∘ 𝐵) = (𝐴 ∘ 𝐵))
Theorem	resco 5881	Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006.)
⊢ ((𝐴 ∘ 𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵 ↾ 𝐶))
Theorem	imaco 5882	Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.)
⊢ ((𝐴 ∘ 𝐵) “ 𝐶) = (𝐴 “ (𝐵 “ 𝐶))
Theorem	rnco 5883	The range of the composition of two classes. (Contributed by NM, 12-Dec-2006.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ ran (𝐴 ∘ 𝐵) = ran (𝐴 ↾ ran 𝐵)
Theorem	rnco2 5884	The range of the composition of two classes. (Contributed by NM, 27-Mar-2008.)
⊢ ran (𝐴 ∘ 𝐵) = (𝐴 “ ran 𝐵)
Theorem	dmco 5885	The domain of a composition. Exercise 27 of [Enderton] p. 53. (Contributed by NM, 4-Feb-2004.)
⊢ dom (𝐴 ∘ 𝐵) = (◡𝐵 “ dom 𝐴)
Theorem	coeq0 5886	A composition of two relations is empty iff there is no overlap between the range of the second and the domain of the first. Useful in combination with coundi 5878 and coundir 5879 to prune meaningless terms in the result. (Contributed by Stefan O'Rear, 8-Oct-2014.)
⊢ ((𝐴 ∘ 𝐵) = ∅ ↔ (dom 𝐴 ∩ ran 𝐵) = ∅)
Theorem	coiun 5887*	Composition with an indexed union. (Contributed by NM, 21-Dec-2008.)
⊢ (𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵) = ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵)
Theorem	cocnvcnv1 5888	A composition is not affected by a double converse of its first argument. (Contributed by NM, 8-Oct-2007.)
⊢ (◡◡𝐴 ∘ 𝐵) = (𝐴 ∘ 𝐵)
Theorem	cocnvcnv2 5889	A composition is not affected by a double converse of its second argument. (Contributed by NM, 8-Oct-2007.)
⊢ (𝐴 ∘ ◡◡𝐵) = (𝐴 ∘ 𝐵)
Theorem	cores2 5890	Absorption of a reverse (preimage) restriction of the second member of a class composition. (Contributed by NM, 11-Dec-2006.)
⊢ (dom 𝐴 ⊆ 𝐶 → (𝐴 ∘ ◡(◡𝐵 ↾ 𝐶)) = (𝐴 ∘ 𝐵))
Theorem	co02 5891	Composition with the empty set. Theorem 20 of [Suppes] p. 63. (Contributed by NM, 24-Apr-2004.)
⊢ (𝐴 ∘ ∅) = ∅
Theorem	co01 5892	Composition with the empty set. (Contributed by NM, 24-Apr-2004.)
⊢ (∅ ∘ 𝐴) = ∅
Theorem	coi1 5893	Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by NM, 22-Apr-2004.)
⊢ (Rel 𝐴 → (𝐴 ∘ I ) = 𝐴)
Theorem	coi2 5894	Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by NM, 22-Apr-2004.)
⊢ (Rel 𝐴 → ( I ∘ 𝐴) = 𝐴)
Theorem	coires1 5895	Composition with a restricted identity relation. (Contributed by FL, 19-Jun-2011.) (Revised by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐴 ∘ ( I ↾ 𝐵)) = (𝐴 ↾ 𝐵)
Theorem	coass 5896	Associative law for class composition. Theorem 27 of [Suppes] p. 64. Also Exercise 21 of [Enderton] p. 53. Interestingly, this law holds for any classes whatsoever, not just functions or even relations. (Contributed by NM, 27-Jan-1997.)
⊢ ((𝐴 ∘ 𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵 ∘ 𝐶))
Theorem	relcnvtr 5897	A relation is transitive iff its converse is transitive. (Contributed by FL, 19-Sep-2011.)
⊢ (Rel 𝑅 → ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ (◡𝑅 ∘ ◡𝑅) ⊆ ◡𝑅))
Theorem	relssdmrn 5898	A relation is included in the Cartesian product of its domain and range. Exercise 4.12(t) of [Mendelson] p. 235. (Contributed by NM, 3-Aug-1994.)
⊢ (Rel 𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴))
Theorem	cnvssrndm 5899	The converse is a subset of the cartesian product of range and domain. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ◡𝐴 ⊆ (ran 𝐴 × dom 𝐴)
Theorem	cossxp 5900	Composition as a subset of the Cartesian product of factors. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)