P. 63 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6201-6300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnvcnv 6201	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 6202	The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007.)
⊢ ◡◡𝐴 = (𝐴 ↾ V)
Theorem	cnvcnvss 6203	The double converse of a class is a subclass. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 23-Jul-2004.)
⊢ ◡◡𝐴 ⊆ 𝐴
Theorem	cnvrescnv 6204	Two ways to express the corestriction of a class. (Contributed by BJ, 28-Dec-2023.)
⊢ ◡(◡𝑅 ↾ 𝐵) = (𝑅 ∩ (V × 𝐵))
Theorem	cnveqb 6205	Equality theorem for converse. (Contributed by FL, 19-Sep-2011.)
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ◡𝐴 = ◡𝐵))
Theorem	cnveq0 6206	A relation empty iff its converse is empty. (Contributed by FL, 19-Sep-2011.)
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ◡𝐴 = ∅))
Theorem	dfrel3 6207	Alternate definition of relation. (Contributed by NM, 14-May-2008.)
⊢ (Rel 𝑅 ↔ (𝑅 ↾ V) = 𝑅)
Theorem	elid 6208*	Characterization of the elements of the identity relation. TODO: reorder theorems to move this theorem and dfrel3 6207 after elrid 6054. (Contributed by BJ, 28-Aug-2022.)
⊢ (𝐴 ∈ I ↔ ∃𝑥 𝐴 = ⟨𝑥, 𝑥⟩)
Theorem	dmresv 6209	The domain of a universal restriction. (Contributed by NM, 14-May-2008.)
⊢ dom (𝐴 ↾ V) = dom 𝐴
Theorem	rnresv 6210	The range of a universal restriction. (Contributed by NM, 14-May-2008.)
⊢ ran (𝐴 ↾ V) = ran 𝐴
Theorem	dfrn4 6211	Range defined in terms of image. (Contributed by NM, 14-May-2008.)
⊢ ran 𝐴 = (𝐴 “ V)
Theorem	csbrn 6212	Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.)
⊢ ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵
Theorem	rescnvcnv 6213	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 6214	The double converse of the restriction of a class. (Contributed by NM, 3-Jun-2007.)
⊢ ◡◡(𝐴 ↾ 𝐵) = (◡◡𝐴 ↾ 𝐵)
Theorem	imacnvcnv 6215	The image of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
⊢ (◡◡𝐴 “ 𝐵) = (𝐴 “ 𝐵)
Theorem	dmsnn0 6216	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 6217	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 6218	The domain of the singleton of the empty set is empty. (Contributed by NM, 30-Jan-2004.)
⊢ dom {∅} = ∅
Theorem	cnvsn0 6219	The converse of the singleton of the empty set is empty. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ ◡{∅} = ∅
Theorem	dmsn0el 6220	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 6221	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 6222	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 6223	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 6224	The domain of an unordered pair of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {𝐴, 𝐶})
Theorem	dmsnop 6225	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 6226	The domain of an unordered pair of ordered pairs. (Contributed by NM, 13-Sep-2011.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {𝐴, 𝐶}
Theorem	dmtpop 6227	The domain of an unordered triple of ordered pairs. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩} = {𝐴, 𝐶, 𝐸}
Theorem	cnvcnvsn 6228	Double converse of a singleton of an ordered pair. (Unlike cnvsn 6235, this does not need any sethood assumptions on 𝐴 and 𝐵.) (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ◡◡{⟨𝐴, 𝐵⟩} = ◡{⟨𝐵, 𝐴⟩}
Theorem	dmsnsnsn 6229	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 6230	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 6231	The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} = {𝐶, 𝐷})
Theorem	cnvsng 6232	Converse of a singleton of an ordered pair. (Contributed by NM, 23-Jan-2015.) (Proof shortened by BJ, 12-Feb-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{⟨𝐴, 𝐵⟩} = {⟨𝐵, 𝐴⟩})
Theorem	rnsnop 6233	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 6234	Extract the first member of an ordered pair. (See op2nda 6237 to extract the second member, op1stb 5477 for an alternate version, and op1st 8007 for the preferred version.) (Contributed by Raph Levien, 4-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ dom {⟨𝐴, 𝐵⟩} = 𝐴
Theorem	cnvsn 6235	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 6236	Extract the second member of an ordered pair. Theorem 5.12(ii) of [Monk1] p. 52. (See op1stb 5477 to extract the first member, op2nda 6237 for an alternate version, and op2nd 8008 for the preferred version.) (Contributed by NM, 25-Nov-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ ∩ ∩ ◡{⟨𝐴, 𝐵⟩} = 𝐵
Theorem	op2nda 6237	Extract the second member of an ordered pair. (See op1sta 6234 to extract the first member, op2ndb 6236 for an alternate version, and op2nd 8008 for the preferred version.) (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ ran {⟨𝐴, 𝐵⟩} = 𝐵
Theorem	opswap 6238	Swap the members of an ordered pair. (Contributed by NM, 14-Dec-2008.) (Revised by Mario Carneiro, 30-Aug-2015.)
⊢ ∪ ◡{⟨𝐴, 𝐵⟩} = ⟨𝐵, 𝐴⟩
Theorem	cnvresima 6239	An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.)
⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴)
Theorem	resdm2 6240	A class restricted to its domain equals its double converse. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 ↾ dom 𝐴) = ◡◡𝐴
Theorem	resdmres 6241	Restriction to the domain of a restriction. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 ↾ dom (𝐴 ↾ 𝐵)) = (𝐴 ↾ 𝐵)
Theorem	resresdm 6242	A restriction by an arbitrary set is a restriction by its domain. (Contributed by AV, 16-Nov-2020.)
⊢ (𝐹 = (𝐸 ↾ 𝐴) → 𝐹 = (𝐸 ↾ dom 𝐹))
Theorem	imadmres 6243	The image of the domain of a restriction. (Contributed by NM, 8-Apr-2007.)
⊢ (𝐴 “ dom (𝐴 ↾ 𝐵)) = (𝐴 “ 𝐵)
Theorem	resdmss 6244	Subset relationship for the domain of a restriction. (Contributed by Scott Fenton, 9-Aug-2024.)
⊢ dom (𝐴 ↾ 𝐵) ⊆ 𝐵
Theorem	resdifdi 6245	Distributive law for restriction over difference. (Contributed by BTernaryTau, 15-Aug-2024.)
⊢ (𝐴 ↾ (𝐵 ∖ 𝐶)) = ((𝐴 ↾ 𝐵) ∖ (𝐴 ↾ 𝐶))
Theorem	resdifdir 6246	Distributive law for restriction over difference. (Contributed by BTernaryTau, 15-Aug-2024.)
⊢ ((𝐴 ∖ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∖ (𝐵 ↾ 𝐶))
Theorem	mptpreima 6247*	The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
Theorem	mptiniseg 6248*	Converse singleton image of a function defined by maps-to. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝐶 ∈ 𝑉 → (◡𝐹 “ {𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐵 = 𝐶})
Theorem	dmmpt 6249	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 6250*	The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ dom 𝐹 ⊆ 𝐴
Theorem	dmmptg 6251*	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	rnmpt0f 6252*	The range of a function in maps-to notation is empty if and only if its domain is empty. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → (ran 𝐹 = ∅ ↔ 𝐴 = ∅))
Theorem	rnmptn0 6253*	The range of a function in maps-to notation is nonempty if the domain is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → ran 𝐹 ≠ ∅)
Theorem	dfco2 6254*	Alternate definition of a class composition, using only one bound variable. (Contributed by NM, 19-Dec-2008.)
⊢ (𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))
Theorem	dfco2a 6255*	Generalization of dfco2 6254, 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 6256	Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶))
Theorem	coundir 6257	Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝐴 ∪ 𝐵) ∘ 𝐶) = ((𝐴 ∘ 𝐶) ∪ (𝐵 ∘ 𝐶))
Theorem	cores 6258	Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (ran 𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ∘ 𝐵) = (𝐴 ∘ 𝐵))
Theorem	resco 6259	Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006.)
⊢ ((𝐴 ∘ 𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵 ↾ 𝐶))
Theorem	imaco 6260	Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.) (Proof shortened by Wolf Lammen, 16-May-2025.)
⊢ ((𝐴 ∘ 𝐵) “ 𝐶) = (𝐴 “ (𝐵 “ 𝐶))
Theorem	rnco 6261	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 6262	The range of the composition of two classes. (Contributed by NM, 27-Mar-2008.)
⊢ ran (𝐴 ∘ 𝐵) = (𝐴 “ ran 𝐵)
Theorem	dmco 6263	The domain of a composition. Exercise 27 of [Enderton] p. 53. (Contributed by NM, 4-Feb-2004.)
⊢ dom (𝐴 ∘ 𝐵) = (◡𝐵 “ dom 𝐴)
Theorem	coeq0 6264	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 6256 and coundir 6257 to prune meaningless terms in the result. (Contributed by Stefan O'Rear, 8-Oct-2014.)
⊢ ((𝐴 ∘ 𝐵) = ∅ ↔ (dom 𝐴 ∩ ran 𝐵) = ∅)
Theorem	coiun 6265*	Composition with an indexed union. (Contributed by NM, 21-Dec-2008.)
⊢ (𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵) = ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵)
Theorem	cocnvcnv1 6266	A composition is not affected by a double converse of its first argument. (Contributed by NM, 8-Oct-2007.)
⊢ (◡◡𝐴 ∘ 𝐵) = (𝐴 ∘ 𝐵)
Theorem	cocnvcnv2 6267	A composition is not affected by a double converse of its second argument. (Contributed by NM, 8-Oct-2007.)
⊢ (𝐴 ∘ ◡◡𝐵) = (𝐴 ∘ 𝐵)
Theorem	cores2 6268	Absorption of a reverse (preimage) restriction of the second member of a class composition. (Contributed by NM, 11-Dec-2006.)
⊢ (dom 𝐴 ⊆ 𝐶 → (𝐴 ∘ ◡(◡𝐵 ↾ 𝐶)) = (𝐴 ∘ 𝐵))
Theorem	co02 6269	Composition with the empty set. Theorem 20 of [Suppes] p. 63. (Contributed by NM, 24-Apr-2004.)
⊢ (𝐴 ∘ ∅) = ∅
Theorem	co01 6270	Composition with the empty set. (Contributed by NM, 24-Apr-2004.)
⊢ (∅ ∘ 𝐴) = ∅
Theorem	coi1 6271	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 6272	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 6273	Composition with a restricted identity relation. (Contributed by FL, 19-Jun-2011.) (Revised by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐴 ∘ ( I ↾ 𝐵)) = (𝐴 ↾ 𝐵)
Theorem	coass 6274	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	relcnvtrg 6275	General form of relcnvtr 6276. (Contributed by Peter Mazsa, 17-Oct-2023.)
⊢ ((Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇) → ((𝑅 ∘ 𝑆) ⊆ 𝑇 ↔ (◡𝑆 ∘ ◡𝑅) ⊆ ◡𝑇))
Theorem	relcnvtr 6276	A relation is transitive iff its converse is transitive. (Contributed by FL, 19-Sep-2011.) (Proof shortened by Peter Mazsa, 17-Oct-2023.)
⊢ (Rel 𝑅 → ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ (◡𝑅 ∘ ◡𝑅) ⊆ ◡𝑅))
Theorem	relssdmrn 6277	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.) (Proof shortened by SN, 23-Dec-2024.)
⊢ (Rel 𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴))
Theorem	relssdmrnOLD 6278	Obsolete version of relssdmrn 6277 as of 23-Dec-2024. (Contributed by NM, 3-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Rel 𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴))
Theorem	resssxp 6279	If the 𝑅-image of a class 𝐴 is a subclass of 𝐵, then the restriction of 𝑅 to 𝐴 is a subset of the Cartesian product of 𝐴 and 𝐵. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝑅 “ 𝐴) ⊆ 𝐵 ↔ (𝑅 ↾ 𝐴) ⊆ (𝐴 × 𝐵))
Theorem	cnvssrndm 6280	The converse is a subset of the cartesian product of range and domain. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ◡𝐴 ⊆ (ran 𝐴 × dom 𝐴)
Theorem	cossxp 6281	Composition as a subset of the Cartesian product of factors. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴)
Theorem	relrelss 6282	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 6283	The membership relation for a relation is inherited by class union. (Contributed by NM, 17-Sep-2006.)
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → ∪ 𝐴 ∈ ∪ 𝑅)
Theorem	relfld 6284	The double union of a relation is its field. (Contributed by NM, 17-Sep-2006.)
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅))
Theorem	relresfld 6285	Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012.)
⊢ (Rel 𝑅 → (𝑅 ↾ ∪ ∪ 𝑅) = 𝑅)
Theorem	relcoi2 6286	Composition with the identity relation restricted to a relation's field. (Contributed by FL, 2-May-2011.)
⊢ (Rel 𝑅 → (( I ↾ ∪ ∪ 𝑅) ∘ 𝑅) = 𝑅)
Theorem	relcoi1 6287	Composition with the identity relation restricted to a relation's field. (Contributed by FL, 8-May-2011.) (Proof shortened by OpenAI, 3-Jul-2020.)
⊢ (Rel 𝑅 → (𝑅 ∘ ( I ↾ ∪ ∪ 𝑅)) = 𝑅)
Theorem	unidmrn 6288	The double union of the converse of a class is its field. (Contributed by NM, 4-Jun-2008.)
⊢ ∪ ∪ ◡𝐴 = (dom 𝐴 ∪ ran 𝐴)
Theorem	relcnvfld 6289	if 𝑅 is a relation, its double union equals the double union of its converse. (Contributed by FL, 5-Jan-2009.)
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = ∪ ∪ ◡𝑅)
Theorem	dfdm2 6290	Alternate definition of domain df-dm 5692 that doesn't require dummy variables. (Contributed by NM, 2-Aug-2010.)
⊢ dom 𝐴 = ∪ ∪ (◡𝐴 ∘ 𝐴)
Theorem	unixp 6291	The double class union of a nonempty Cartesian product is the union of it members. (Contributed by NM, 17-Sep-2006.)
⊢ ((𝐴 × 𝐵) ≠ ∅ → ∪ ∪ (𝐴 × 𝐵) = (𝐴 ∪ 𝐵))
Theorem	unixp0 6292	A Cartesian product is empty iff its union is empty. (Contributed by NM, 20-Sep-2006.)
⊢ ((𝐴 × 𝐵) = ∅ ↔ ∪ (𝐴 × 𝐵) = ∅)
Theorem	unixpid 6293	Field of a Cartesian square. (Contributed by FL, 10-Oct-2009.)
⊢ ∪ ∪ (𝐴 × 𝐴) = 𝐴
Theorem	ressn 6294	Restriction of a class to a singleton. (Contributed by Mario Carneiro, 28-Dec-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (𝐴 ↾ {𝐵}) = ({𝐵} × (𝐴 “ {𝐵}))
Theorem	cnviin 6295*	The converse of an intersection is the intersection of the converse. (Contributed by FL, 15-Oct-2012.)
⊢ (𝐴 ≠ ∅ → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵)
Theorem	cnvpo 6296	The converse of a partial order is a partial order. (Contributed by NM, 15-Jun-2005.)
⊢ (𝑅 Po 𝐴 ↔ ◡𝑅 Po 𝐴)
Theorem	cnvso 6297	The converse of a strict order relation is a strict order relation. (Contributed by NM, 15-Jun-2005.)
⊢ (𝑅 Or 𝐴 ↔ ◡𝑅 Or 𝐴)
Theorem	xpco 6298	Composition of two Cartesian products. (Contributed by Thierry Arnoux, 17-Nov-2017.)
⊢ (𝐵 ≠ ∅ → ((𝐵 × 𝐶) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐶))
Theorem	xpcoid 6299	Composition of two Cartesian squares. (Contributed by Thierry Arnoux, 14-Jan-2018.)
⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) = (𝐴 × 𝐴)
Theorem	elsnxp 6300*	Membership in a Cartesian product with a singleton. (Contributed by Thierry Arnoux, 10-Apr-2020.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ (𝑋 ∈ 𝑉 → (𝑍 ∈ ({𝑋} × 𝐴) ↔ ∃𝑦 ∈ 𝐴 𝑍 = ⟨𝑋, 𝑦⟩))