P. 49 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4801-4900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	djudisj 4801*	Disjoint unions with disjoint index sets are disjoint. (Contributed by Stefan O'Rear, 21-Nov-2014.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐶) ∩ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝐷)) = ∅)
Theorem	resdisj 4802	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	rnxpm 4803*	The range of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37, with non-empty changed to inhabited. (Contributed by Jim Kingdon, 12-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ran (𝐴 × 𝐵) = 𝐵)
Theorem	dmxpss 4804	The domain of a cross product is a subclass of the first factor. (Contributed by NM, 19-Mar-2007.)
⊢ dom (𝐴 × 𝐵) ⊆ 𝐴
Theorem	rnxpss 4805	The range of a cross 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 4806	The range of a square cross product. (Contributed by FL, 17-May-2010.)
⊢ ran (𝐴 × 𝐴) = 𝐴
Theorem	ssxpbm 4807*	A cross-product subclass relationship is equivalent to the relationship for its components. (Contributed by Jim Kingdon, 12-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ (𝐴 × 𝐵) → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷)))
Theorem	ssxp1 4808*	Cross product subset cancellation. (Contributed by Jim Kingdon, 14-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐴 × 𝐶) ⊆ (𝐵 × 𝐶) ↔ 𝐴 ⊆ 𝐵))
Theorem	ssxp2 4809*	Cross product subset cancellation. (Contributed by Jim Kingdon, 14-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐶 × 𝐴) ⊆ (𝐶 × 𝐵) ↔ 𝐴 ⊆ 𝐵))
Theorem	xp11m 4810*	The cross product of inhabited classes is one-to-one. (Contributed by Jim Kingdon, 13-Dec-2018.)
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) → ((𝐴 × 𝐵) = (𝐶 × 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	xpcanm 4811*	Cancellation law for cross-product. (Contributed by Jim Kingdon, 14-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐶 × 𝐴) = (𝐶 × 𝐵) ↔ 𝐴 = 𝐵))
Theorem	xpcan2m 4812*	Cancellation law for cross-product. (Contributed by Jim Kingdon, 14-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐴 × 𝐶) = (𝐵 × 𝐶) ↔ 𝐴 = 𝐵))
Theorem	xpexr2m 4813*	If a nonempty cross product is a set, so are both of its components. (Contributed by Jim Kingdon, 14-Dec-2018.)
⊢ (((𝐴 × 𝐵) ∈ 𝐶 ∧ ∃𝑥 𝑥 ∈ (𝐴 × 𝐵)) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	ssrnres 4814	Subset of the range of a restriction. (Contributed by NM, 16-Jan-2006.)
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) ↔ ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵)
Theorem	rninxp 4815*	Range of the intersection with a cross product. (Contributed by NM, 17-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐶𝑦)
Theorem	dminxp 4816*	Domain of the intersection with a cross product. (Contributed by NM, 17-Jan-2006.)
⊢ (dom (𝐶 ∩ (𝐴 × 𝐵)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥𝐶𝑦)
Theorem	imainrect 4817	Image of a relation restricted to a rectangular region. (Contributed by Stefan O'Rear, 19-Feb-2015.)
⊢ ((𝐺 ∩ (𝐴 × 𝐵)) “ 𝑌) = ((𝐺 “ (𝑌 ∩ 𝐴)) ∩ 𝐵)
Theorem	xpima1 4818	The image by a cross product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) “ 𝐶) = ∅)
Theorem	xpima2m 4819*	The image by a cross product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
⊢ (∃𝑥 𝑥 ∈ (𝐴 ∩ 𝐶) → ((𝐴 × 𝐵) “ 𝐶) = 𝐵)
Theorem	xpimasn 4820	The image of a singleton by a cross product. (Contributed by Thierry Arnoux, 14-Jan-2018.)
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵)
Theorem	cnvcnv3 4821*	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 4822	Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.)
⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)
Theorem	dfrel4v 4823*	A relation can be expressed as the set of ordered pairs in it. (Contributed by Mario Carneiro, 16-Aug-2015.)
⊢ (Rel 𝑅 ↔ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦})
Theorem	cnvcnv 4824	The double converse of a class strips out all elements that are not ordered pairs. (Contributed by NM, 8-Dec-2003.)
⊢ ◡◡𝐴 = (𝐴 ∩ (V × V))
Theorem	cnvcnv2 4825	The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007.)
⊢ ◡◡𝐴 = (𝐴 ↾ V)
Theorem	cnvcnvss 4826	The double converse of a class is a subclass. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 23-Jul-2004.)
⊢ ◡◡𝐴 ⊆ 𝐴
Theorem	cnveqb 4827	Equality theorem for converse. (Contributed by FL, 19-Sep-2011.)
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ◡𝐴 = ◡𝐵))
Theorem	cnveq0 4828	A relation empty iff its converse is empty. (Contributed by FL, 19-Sep-2011.)
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ◡𝐴 = ∅))
Theorem	dfrel3 4829	Alternate definition of relation. (Contributed by NM, 14-May-2008.)
⊢ (Rel 𝑅 ↔ (𝑅 ↾ V) = 𝑅)
Theorem	dmresv 4830	The domain of a universal restriction. (Contributed by NM, 14-May-2008.)
⊢ dom (𝐴 ↾ V) = dom 𝐴
Theorem	rnresv 4831	The range of a universal restriction. (Contributed by NM, 14-May-2008.)
⊢ ran (𝐴 ↾ V) = ran 𝐴
Theorem	dfrn4 4832	Range defined in terms of image. (Contributed by NM, 14-May-2008.)
⊢ ran 𝐴 = (𝐴 “ V)
Theorem	csbrng 4833	Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵)
Theorem	rescnvcnv 4834	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 4835	The double converse of the restriction of a class. (Contributed by NM, 3-Jun-2007.)
⊢ ◡◡(𝐴 ↾ 𝐵) = (◡◡𝐴 ↾ 𝐵)
Theorem	imacnvcnv 4836	The image of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
⊢ (◡◡𝐴 “ 𝐵) = (𝐴 “ 𝐵)
Theorem	dmsnm 4837*	The domain of a singleton is inhabited iff the singleton argument is an ordered pair. (Contributed by Jim Kingdon, 15-Dec-2018.)
⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥 𝑥 ∈ dom {𝐴})
Theorem	rnsnm 4838*	The range of a singleton is inhabited iff the singleton argument is an ordered pair. (Contributed by Jim Kingdon, 15-Dec-2018.)
⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥 𝑥 ∈ ran {𝐴})
Theorem	dmsn0 4839	The domain of the singleton of the empty set is empty. (Contributed by NM, 30-Jan-2004.)
⊢ dom {∅} = ∅
Theorem	cnvsn0 4840	The converse of the singleton of the empty set is empty. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ ◡{∅} = ∅
Theorem	dmsn0el 4841	The domain of a singleton is empty if the singleton's argument contains the empty set. (Contributed by NM, 15-Dec-2008.)
⊢ (∅ ∈ 𝐴 → dom {𝐴} = ∅)
Theorem	relsn2m 4842*	A singleton is a relation iff it has an inhabited domain. (Contributed by Jim Kingdon, 16-Dec-2018.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Rel {𝐴} ↔ ∃𝑥 𝑥 ∈ dom {𝐴})
Theorem	dmsnopg 4843	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	dmpropg 4844	The domain of an unordered pair of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {𝐴, 𝐶})
Theorem	dmsnop 4845	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 4846	The domain of an unordered pair of ordered pairs. (Contributed by NM, 13-Sep-2011.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {𝐴, 𝐶}
Theorem	dmtpop 4847	The domain of an unordered triple of ordered pairs. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩} = {𝐴, 𝐶, 𝐸}
Theorem	cnvcnvsn 4848	Double converse of a singleton of an ordered pair. (Unlike cnvsn 4854, this does not need any sethood assumptions on 𝐴 and 𝐵.) (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ◡◡{⟨𝐴, 𝐵⟩} = ◡{⟨𝐵, 𝐴⟩}
Theorem	dmsnsnsng 4849	The domain of the singleton of the singleton of a singleton. (Contributed by Jim Kingdon, 16-Dec-2018.)
⊢ (𝐴 ∈ V → dom {{{𝐴}}} = {𝐴})
Theorem	rnsnopg 4850	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 4851	The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} = {𝐶, 𝐷})
Theorem	rnsnop 4852	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 4853	Extract the first member of an ordered pair. (See op2nda 4856 to extract the second member and op1stb 4256 for an alternate version.) (Contributed by Raph Levien, 4-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ dom {⟨𝐴, 𝐵⟩} = 𝐴
Theorem	cnvsn 4854	Converse of a singleton of an ordered pair. (Contributed by NM, 11-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ◡{⟨𝐴, 𝐵⟩} = {⟨𝐵, 𝐴⟩}
Theorem	op2ndb 4855	Extract the second member of an ordered pair. Theorem 5.12(ii) of [Monk1] p. 52. (See op1stb 4256 to extract the first member and op2nda 4856 for an alternate version.) (Contributed by NM, 25-Nov-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ ∩ ∩ ◡{⟨𝐴, 𝐵⟩} = 𝐵
Theorem	op2nda 4856	Extract the second member of an ordered pair. (See op1sta 4853 to extract the first member and op2ndb 4855 for an alternate version.) (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ ran {⟨𝐴, 𝐵⟩} = 𝐵
Theorem	cnvsng 4857	Converse of a singleton of an ordered pair. (Contributed by NM, 23-Jan-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{⟨𝐴, 𝐵⟩} = {⟨𝐵, 𝐴⟩})
Theorem	opswapg 4858	Swap the members of an ordered pair. (Contributed by Jim Kingdon, 16-Dec-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ ◡{⟨𝐴, 𝐵⟩} = ⟨𝐵, 𝐴⟩)
Theorem	elxp4 4859	Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp5 4860. (Contributed by NM, 17-Feb-2004.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
Theorem	elxp5 4860	Membership in a cross product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 4859 when the double intersection does not create class existence problems (caused by int0 3671). (Contributed by NM, 1-Aug-2004.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
Theorem	cnvresima 4861	An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.)
⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴)
Theorem	resdm2 4862	A class restricted to its domain equals its double converse. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 ↾ dom 𝐴) = ◡◡𝐴
Theorem	resdmres 4863	Restriction to the domain of a restriction. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 ↾ dom (𝐴 ↾ 𝐵)) = (𝐴 ↾ 𝐵)
Theorem	imadmres 4864	The image of the domain of a restriction. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 “ dom (𝐴 ↾ 𝐵)) = (𝐴 “ 𝐵)
Theorem	mptpreima 4865*	The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
Theorem	mptiniseg 4866*	Converse singleton image of a function defined by maps-to. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝐶 ∈ 𝑉 → (◡𝐹 “ {𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐵 = 𝐶})
Theorem	dmmpt 4867	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 4868*	The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ dom 𝐹 ⊆ 𝐴
Theorem	dmmptg 4869*	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 4870	A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.)
⊢ Rel (𝐴 ∘ 𝐵)
Theorem	dfco2 4871*	Alternate definition of a class composition, using only one bound variable. (Contributed by NM, 19-Dec-2008.)
⊢ (𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))
Theorem	dfco2a 4872*	Generalization of dfco2 4871, 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 4873	Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶))
Theorem	coundir 4874	Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝐴 ∪ 𝐵) ∘ 𝐶) = ((𝐴 ∘ 𝐶) ∪ (𝐵 ∘ 𝐶))
Theorem	cores 4875	Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (ran 𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ∘ 𝐵) = (𝐴 ∘ 𝐵))
Theorem	resco 4876	Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006.)
⊢ ((𝐴 ∘ 𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵 ↾ 𝐶))
Theorem	imaco 4877	Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.)
⊢ ((𝐴 ∘ 𝐵) “ 𝐶) = (𝐴 “ (𝐵 “ 𝐶))
Theorem	rnco 4878	The range of the composition of two classes. (Contributed by NM, 12-Dec-2006.)
⊢ ran (𝐴 ∘ 𝐵) = ran (𝐴 ↾ ran 𝐵)
Theorem	rnco2 4879	The range of the composition of two classes. (Contributed by NM, 27-Mar-2008.)
⊢ ran (𝐴 ∘ 𝐵) = (𝐴 “ ran 𝐵)
Theorem	dmco 4880	The domain of a composition. Exercise 27 of [Enderton] p. 53. (Contributed by NM, 4-Feb-2004.)
⊢ dom (𝐴 ∘ 𝐵) = (◡𝐵 “ dom 𝐴)
Theorem	coiun 4881*	Composition with an indexed union. (Contributed by NM, 21-Dec-2008.)
⊢ (𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵) = ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵)
Theorem	cocnvcnv1 4882	A composition is not affected by a double converse of its first argument. (Contributed by NM, 8-Oct-2007.)
⊢ (◡◡𝐴 ∘ 𝐵) = (𝐴 ∘ 𝐵)
Theorem	cocnvcnv2 4883	A composition is not affected by a double converse of its second argument. (Contributed by NM, 8-Oct-2007.)
⊢ (𝐴 ∘ ◡◡𝐵) = (𝐴 ∘ 𝐵)
Theorem	cores2 4884	Absorption of a reverse (preimage) restriction of the second member of a class composition. (Contributed by NM, 11-Dec-2006.)
⊢ (dom 𝐴 ⊆ 𝐶 → (𝐴 ∘ ◡(◡𝐵 ↾ 𝐶)) = (𝐴 ∘ 𝐵))
Theorem	co02 4885	Composition with the empty set. Theorem 20 of [Suppes] p. 63. (Contributed by NM, 24-Apr-2004.)
⊢ (𝐴 ∘ ∅) = ∅
Theorem	co01 4886	Composition with the empty set. (Contributed by NM, 24-Apr-2004.)
⊢ (∅ ∘ 𝐴) = ∅
Theorem	coi1 4887	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 4888	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 4889	Composition with a restricted identity relation. (Contributed by FL, 19-Jun-2011.) (Revised by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐴 ∘ ( I ↾ 𝐵)) = (𝐴 ↾ 𝐵)
Theorem	coass 4890	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 4891	A relation is transitive iff its converse is transitive. (Contributed by FL, 19-Sep-2011.)
⊢ (Rel 𝑅 → ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ (◡𝑅 ∘ ◡𝑅) ⊆ ◡𝑅))
Theorem	relssdmrn 4892	A relation is included in the cross 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 4893	The converse is a subset of the cartesian product of range and domain. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ◡𝐴 ⊆ (ran 𝐴 × dom 𝐴)
Theorem	cossxp 4894	Composition as a subset of the cross product of factors. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)
Theorem	relrelss 4895	Two ways to describe the structure of a two-place operation. (Contributed by NM, 17-Dec-2008.)
⊢ ((Rel 𝐴 ∧ Rel dom 𝐴) ↔ 𝐴 ⊆ ((V × V) × V))
Theorem	unielrel 4896	The membership relation for a relation is inherited by class union. (Contributed by NM, 17-Sep-2006.)
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → ∪ 𝐴 ∈ ∪ 𝑅)
Theorem	relfld 4897	The double union of a relation is its field. (Contributed by NM, 17-Sep-2006.)
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅))
Theorem	relresfld 4898	Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012.)
⊢ (Rel 𝑅 → (𝑅 ↾ ∪ ∪ 𝑅) = 𝑅)
Theorem	relcoi2 4899	Composition with the identity relation restricted to a relation's field. (Contributed by FL, 2-May-2011.)
⊢ (Rel 𝑅 → (( I ↾ ∪ ∪ 𝑅) ∘ 𝑅) = 𝑅)
Theorem	relcoi1 4900	Composition with the identity relation restricted to a relation's field. (Contributed by FL, 8-May-2011.)
⊢ (Rel 𝑅 → (𝑅 ∘ ( I ↾ ∪ ∪ 𝑅)) = 𝑅)