P. 51 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 5001-5100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iss 5001	A subclass of the identity function is the identity function restricted to its domain. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 13-Dec-2003.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ (A ⊆ I ↔ A = ( I ↾ dom A))
Theorem	resopab2 5002*	Restriction of a class abstraction of ordered pairs. (Contributed by set.mm contributors, 24-Aug-2007.)
⊢ (A ⊆ B → ({⟨x, y⟩ ∣ (x ∈ B ∧ φ)} ↾ A) = {⟨x, y⟩ ∣ (x ∈ A ∧ φ)})
Theorem	dfres2 5003*	Alternate definition of the restriction operation. (Contributed by Mario Carneiro, 5-Nov-2013.)
⊢ (R ↾ A) = {⟨x, y⟩ ∣ (x ∈ A ∧ xRy)}
Theorem	opabresid 5004*	The restricted identity expressed with the class builder. (Contributed by FL, 25-Apr-2012.)
⊢ {⟨x, y⟩ ∣ (x ∈ A ∧ y = x)} = ( I ↾ A)
Theorem	dmresi 5005	The domain of a restricted identity function. (Contributed by set.mm contributors, 27-Aug-2004.)
⊢ dom ( I ↾ A) = A
Theorem	resid 5006	Any class restricted to the universe is itself. (Contributed by set.mm contributors, 16-Mar-2004.) (Revised by Scott Fenton, 18-Apr-2021.)
⊢ (A ↾ V) = A
Theorem	resima 5007	A restriction to an image. (Contributed by set.mm contributors, 29-Sep-2004.)
⊢ ((A ↾ B) “ B) = (A “ B)
Theorem	resima2 5008	Image under a restricted class. (Contributed by FL, 31-Aug-2009.)
⊢ (B ⊆ C → ((A ↾ C) “ B) = (A “ B))
Theorem	imadmrn 5009	The image of the domain of a class is the range of the class. (Contributed by set.mm contributors, 14-Aug-1994.)
⊢ (A “ dom A) = ran A
Theorem	imassrn 5010	The image of a class is a subset of its range. Theorem 3.16(xi) of [Monk1] p. 39. (Contributed by set.mm contributors, 31-Mar-1995.)
⊢ (A “ B) ⊆ ran A
Theorem	imai 5011	Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38. (Contributed by set.mm contributors, 30-Apr-1998.)
⊢ ( I “ A) = A
Theorem	rnresi 5012	The range of the restricted identity function. (Contributed by set.mm contributors, 27-Aug-2004.)
⊢ ran ( I ↾ A) = A
Theorem	resiima 5013	The image of a restriction of the identity function. (Contributed by FL, 31-Dec-2006.)
⊢ (B ⊆ A → (( I ↾ A) “ B) = B)
Theorem	ima0 5014	Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by set.mm contributors, 20-May-1998.)
⊢ (A “ ∅) = ∅
Theorem	0ima 5015	Image under the empty relation. (Contributed by FL, 11-Jan-2007.)
⊢ (∅ “ A) = ∅
Theorem	imadisj 5016	A class whose image under another is empty is disjoint with the other's domain. (Contributed by FL, 24-Jan-2007.)
⊢ ((A “ B) = ∅ ↔ (dom A ∩ B) = ∅)
Theorem	cnvimass 5017	A preimage under any class is included in the domain of the class. (Contributed by FL, 29-Jan-2007.)
⊢ (◡A “ B) ⊆ dom A
Theorem	cnvimarndm 5018	The preimage of the range of a class is the domain of the class. (Contributed by Jeff Hankins, 15-Jul-2009.)
⊢ (◡A “ ran A) = dom A
Theorem	imasn 5019*	The image of a singleton. (Contributed by set.mm contributors, 9-Jan-2015.)
⊢ (R “ {A}) = {y ∣ ARy}
Theorem	elimasn 5020	Membership in an image of a singleton. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 15-Mar-2004.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ (C ∈ (A “ {B}) ↔ ⟨B, C⟩ ∈ A)
Theorem	eliniseg 5021	Membership in an initial segment. The idiom (◡A “ {B}), meaning {x ∣ xAB}, is used to specify an initial segment in (for example) Definition 6.21 of [TakeutiZaring] p. 30. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 28-Apr-2004.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ (C ∈ (◡A “ {B}) ↔ CAB)
Theorem	epini 5022	Any set is equal to its preimage under the converse epsilon relation. (Contributed by Mario Carneiro, 9-Mar-2013.)
⊢ A ∈ V    ⇒   ⊢ (◡ E “ {A}) = A
Theorem	iniseg 5023*	An idiom that signifies an initial segment of an ordering, used, for example, in Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by set.mm contributors, 28-Apr-2004.)
⊢ (◡A “ {B}) = {x ∣ xAB}
Theorem	imass1 5024	Subset theorem for image. (Contributed by set.mm contributors, 16-Mar-2004.)
⊢ (A ⊆ B → (A “ C) ⊆ (B “ C))
Theorem	imass2 5025	Subset theorem for image. Exercise 22(a) of [Enderton] p. 53. (Contributed by set.mm contributors, 22-Mar-1998.)
⊢ (A ⊆ B → (C “ A) ⊆ (C “ B))
Theorem	ndmima 5026	The image of a singleton outside the domain is empty. (Contributed by set.mm contributors, 22-May-1998.)
⊢ (¬ A ∈ dom B → (B “ {A}) = ∅)
Theorem	cotr 5027*	Two ways of saying a relation is transitive. Definition of transitivity in [Schechter] p. 51. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 27-Dec-1996.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ ((R ∘ R) ⊆ R ↔ ∀x∀y∀z((xRy ∧ yRz) → xRz))
Theorem	cnvsym 5028*	Two ways of saying a relation is symmetric. Similar to definition of symmetry in [Schechter] p. 51. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 28-Dec-1996.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ (◡R ⊆ R ↔ ∀x∀y(xRy → yRx))
Theorem	intasym 5029*	Two ways of saying a relation is antisymmetric. Definition of antisymmetry in [Schechter] p. 51. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 9-Sep-2004.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ ((R ∩ ◡R) ⊆ I ↔ ∀x∀y((xRy ∧ yRx) → x = y))
Theorem	intirr 5030*	Two ways of saying a relation is irreflexive. Definition of irreflexivity in [Schechter] p. 51. (Contributed by NM, 9-Sep-2004.) (Revised by Andrew Salmon, 27-Aug-2011.)
⊢ ((R ∩ I ) = ∅ ↔ ∀x ¬ xRx)
Theorem	cnvopab 5031*	The converse of a class abstraction of ordered pairs. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 11-Dec-2003.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ ◡{⟨x, y⟩ ∣ φ} = {⟨y, x⟩ ∣ φ}
Theorem	cnv0 5032	The converse of the empty set. (Contributed by set.mm contributors, 6-Apr-1998.)
⊢ ◡∅ = ∅
Theorem	cnvi 5033	The converse of the identity relation. Theorem 3.7(ii) of [Monk1] p. 36. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 26-Apr-1998.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ ◡ I = I
Theorem	cnvun 5034	The converse of a union is the union of converses. Theorem 16 of [Suppes] p. 62. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 25-Mar-1998.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ ◡(A ∪ B) = (◡A ∪ ◡B)
Theorem	cnvdif 5035	Distributive law for converse over set difference. (Contributed by set.mm contributors, 26-Jun-2014.)
⊢ ◡(A ∖ B) = (◡A ∖ ◡B)
Theorem	cnvin 5036	Distributive law for converse over intersection. Theorem 15 of [Suppes] p. 62. (Contributed by set.mm contributors, 25-Mar-1998.) (Revised by set.mm contributors, 26-Jun-2014.)
⊢ ◡(A ∩ B) = (◡A ∩ ◡B)
Theorem	rnun 5037	Distributive law for range over union. Theorem 8 of [Suppes] p. 60. (Contributed by set.mm contributors, 24-Mar-1998.)
⊢ ran (A ∪ B) = (ran A ∪ ran B)
Theorem	rnin 5038	The range of an intersection belongs the intersection of ranges. Theorem 9 of [Suppes] p. 60. (Contributed by set.mm contributors, 15-Sep-2004.)
⊢ ran (A ∩ B) ⊆ (ran A ∩ ran B)
Theorem	rnuni 5039*	The range of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by set.mm contributors, 17-Mar-2004.)
⊢ ran ∪A = ∪x ∈ A ran x
Theorem	imaundi 5040	Distributive law for image over union. Theorem 35 of [Suppes] p. 65. (Contributed by set.mm contributors, 30-Sep-2002.)
⊢ (A “ (B ∪ C)) = ((A “ B) ∪ (A “ C))
Theorem	imaundir 5041	The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.)
⊢ ((A ∪ B) “ C) = ((A “ C) ∪ (B “ C))
Theorem	dminss 5042	An upper bound for intersection with a domain. Theorem 40 of [Suppes] p. 66, who calls it "somewhat surprising." (Contributed by set.mm contributors, 11-Aug-2004.)
⊢ (dom R ∩ A) ⊆ (◡R “ (R “ A))
Theorem	imainss 5043	An upper bound for intersection with an image. Theorem 41 of [Suppes] p. 66. (Contributed by set.mm contributors, 11-Aug-2004.)
⊢ ((R “ A) ∩ B) ⊆ (R “ (A ∩ (◡R “ B)))
Theorem	cnvxp 5044	The converse of a cross product. Exercise 11 of [Suppes] p. 67. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 14-Aug-1999.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ ◡(A × B) = (B × A)
Theorem	xp0 5045	The cross product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by set.mm contributors, 12-Apr-2004.)
⊢ (A × ∅) = ∅
Theorem	xpnz 5046	The cross product of nonempty classes is nonempty. (Variation of a theorem contributed by Raph Levien, 30-Jun-2006.) (Contributed by set.mm contributors, 30-Jun-2006.) (Revised by set.mm contributors, 19-Apr-2007.)
⊢ ((A ≠ ∅ ∧ B ≠ ∅) ↔ (A × B) ≠ ∅)
Theorem	xpeq0 5047	At least one member of an empty cross product is empty. (Contributed by set.mm contributors, 27-Aug-2006.)
⊢ ((A × B) = ∅ ↔ (A = ∅ ∨ B = ∅))
Theorem	xpdisj1 5048	Cross products with disjoint sets are disjoint. (Contributed by set.mm contributors, 13-Sep-2004.)
⊢ ((A ∩ B) = ∅ → ((A × C) ∩ (B × D)) = ∅)
Theorem	xpdisj2 5049	Cross products with disjoint sets are disjoint. (Contributed by set.mm contributors, 13-Sep-2004.)
⊢ ((A ∩ B) = ∅ → ((C × A) ∩ (D × B)) = ∅)
Theorem	xpsndisj 5050	Cross products with two different singletons are disjoint. (Contributed by set.mm contributors, 28-Jul-2004.) (Revised by set.mm contributors, 3-Jun-2007.)
⊢ (B ≠ D → ((A × {B}) ∩ (C × {D})) = ∅)
Theorem	resdisj 5051	A double restriction to disjoint classes is the empty set. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 7-Oct-2004.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ ((A ∩ B) = ∅ → ((C ↾ A) ↾ B) = ∅)
Theorem	rnxp 5052	The range of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37. (Contributed by set.mm contributors, 12-Apr-2004.) (Revised by set.mm contributors, 9-Apr-2007.)
⊢ (A ≠ ∅ → ran (A × B) = B)
Theorem	dmxpss 5053	The domain of a cross product is a subclass of the first factor. (Contributed by set.mm contributors, 19-Mar-2007.)
⊢ dom (A × B) ⊆ A
Theorem	rnxpss 5054	The range of a cross product is a subclass of the second factor. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 16-Jan-2006.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ ran (A × B) ⊆ B
Theorem	rnxpid 5055	The range of a square cross product. (Contributed by FL, 17-May-2010.)
⊢ ran (A × A) = A
Theorem	ssxpb 5056	A cross-product subclass relationship is equivalent to the relationship for it components. (Contributed by set.mm contributors, 17-Dec-2008.)
⊢ ((A × B) ≠ ∅ → ((A × B) ⊆ (C × D) ↔ (A ⊆ C ∧ B ⊆ D)))
Theorem	xp11 5057	The cross product of nonempty classes is one-to-one. (Contributed by set.mm contributors, 31-May-2008.)
⊢ ((A ≠ ∅ ∧ B ≠ ∅) → ((A × B) = (C × D) ↔ (A = C ∧ B = D)))
Theorem	xpcan 5058	Cancellation law for cross-product. (Contributed by set.mm contributors, 30-Aug-2011.)
⊢ (C ≠ ∅ → ((C × A) = (C × B) ↔ A = B))
Theorem	xpcan2 5059	Cancellation law for cross-product. (Contributed by set.mm contributors, 30-Aug-2011.)
⊢ (C ≠ ∅ → ((A × C) = (B × C) ↔ A = B))
Theorem	ssrnres 5060	Subset of the range of a restriction. (Contributed by set.mm contributors, 16-Jan-2006.)
⊢ (B ⊆ ran (C ↾ A) ↔ ran (C ∩ (A × B)) = B)
Theorem	rninxp 5061*	Range of the intersection with a cross product. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 17-Jan-2006.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ (ran (C ∩ (A × B)) = B ↔ ∀y ∈ B ∃x ∈ A xCy)
Theorem	dminxp 5062*	Domain of the intersection with a cross product. (Contributed by set.mm contributors, 17-Jan-2006.)
⊢ (dom (C ∩ (A × B)) = A ↔ ∀x ∈ A ∃y ∈ B xCy)
Theorem	cnvcnv 5063	The double converse of a class is the original class. (Contributed by Scott Fenton, 17-Apr-2021.)
⊢ ◡◡R = R
Theorem	cnveqb 5064	Equality theorem for converse. (Contributed by FL, 19-Sep-2011.) (Revised by Scott Fenton, 17-Apr-2021.)
⊢ (A = B ↔ ◡A = ◡B)
Theorem	dmsnn0 5065	The domain of a singleton is nonzero iff the singleton argument is a set. (Contributed by NM, 14-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Scott Fenton, 19-Apr-2021.)
⊢ (A ∈ V ↔ dom {A} ≠ ∅)
Theorem	rnsnn0 5066	The range of a singleton is nonzero iff the singleton argument is a set. (Contributed by set.mm contributors, 14-Dec-2008.) (Revised by Scott Fenton, 19-Apr-2021.)
⊢ (A ∈ V ↔ ran {A} ≠ ∅)
Theorem	dmsnopg 5067	The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (B ∈ V → dom {⟨A, B⟩} = {A})
Theorem	dmsnopss 5068	The domain of a singleton of an ordered pair is a subset of the singleton of the first member (with no sethood assumptions on B). (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ dom {⟨A, B⟩} ⊆ {A}
Theorem	dmpropg 5069	The domain of an unordered pair of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ((B ∈ V ∧ D ∈ W) → dom {⟨A, B⟩, ⟨C, D⟩} = {A, C})
Theorem	dmsnop 5070	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.)
⊢ B ∈ V    ⇒   ⊢ dom {⟨A, B⟩} = {A}
Theorem	dmprop 5071	The domain of an unordered pair of ordered pairs. (Contributed by NM, 13-Sep-2011.)
⊢ B ∈ V    &   ⊢ D ∈ V    ⇒   ⊢ dom {⟨A, B⟩, ⟨C, D⟩} = {A, C}
Theorem	dmtpop 5072	The domain of an unordered triple of ordered pairs. (Contributed by NM, 14-Sep-2011.)
⊢ B ∈ V    &   ⊢ D ∈ V    &   ⊢ F ∈ V    ⇒   ⊢ dom {⟨A, B⟩, ⟨C, D⟩, ⟨E, F⟩} = {A, C, E}
Theorem	op1sta 5073	Extract the first member of an ordered pair. (Contributed by Raph Levien, 4-Dec-2003.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ∪dom {⟨A, B⟩} = A
Theorem	cnvsn 5074	Converse of a singleton of an ordered pair. (Contributed by NM, 11-May-1998.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ◡{⟨A, B⟩} = {⟨B, A⟩}
Theorem	opswap 5075	Swap the members of an ordered pair. (Contributed by set.mm contributors, 14-Dec-2008.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ∪◡{⟨A, B⟩} = ⟨B, A⟩
Theorem	rnsnop 5076	The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by set.mm contributors, 24-Jul-2004.)
⊢ A ∈ V    ⇒   ⊢ ran {⟨A, B⟩} = {B}
Theorem	op2nda 5077	Extract the second member of an ordered pair. (Contributed by set.mm contributors, 9-Jan-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ∪ran {⟨A, B⟩} = B
Theorem	cnvresima 5078	An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.)
⊢ (◡(F ↾ A) “ B) = ((◡F “ B) ∩ A)
Theorem	resdmres 5079	Restriction to the domain of a restriction. (Contributed by set.mm contributors, 8-Apr-2007.)
⊢ (A ↾ dom (A ↾ B)) = (A ↾ B)
Theorem	imadmres 5080	The image of the domain of a restriction. (Contributed by set.mm contributors, 8-Apr-2007.)
⊢ (A “ dom (A ↾ B)) = (A “ B)
Theorem	dfco2 5081*	Alternate definition of a class composition, using only one bound variable. (Contributed by set.mm contributors, 19-Dec-2008.)
⊢ (A ∘ B) = ∪x ∈ V ((◡B “ {x}) × (A “ {x}))
Theorem	dfco2a 5082*	Generalization of dfco2 5081, where C can have any value between dom A ∩ ran B and V. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 21-Dec-2008.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ ((dom A ∩ ran B) ⊆ C → (A ∘ B) = ∪x ∈ C ((◡B “ {x}) × (A “ {x})))
Theorem	coundi 5083	Class composition distributes over union. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 21-Dec-2008.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ (A ∘ (B ∪ C)) = ((A ∘ B) ∪ (A ∘ C))
Theorem	coundir 5084	Class composition distributes over union. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 21-Dec-2008.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ ((A ∪ B) ∘ C) = ((A ∘ C) ∪ (B ∘ C))
Theorem	cores 5085	Restricted first member of a class composition. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 12-Oct-2004.) (Revised by set.mm contributors, 27-Aug-2011.)
⊢ (ran B ⊆ C → ((A ↾ C) ∘ B) = (A ∘ B))
Theorem	resco 5086	Associative law for the restriction of a composition. (Contributed by set.mm contributors, 12-Dec-2006.)
⊢ ((A ∘ B) ↾ C) = (A ∘ (B ↾ C))
Theorem	imaco 5087	Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.)
⊢ ((A ∘ B) “ C) = (A “ (B “ C))
Theorem	rnco 5088	The range of the composition of two classes. (Contributed by set.mm contributors, 12-Dec-2006.)
⊢ ran (A ∘ B) = ran (A ↾ ran B)
Theorem	rnco2 5089	The range of the composition of two classes. (Contributed by set.mm contributors, 27-Mar-2008.)
⊢ ran (A ∘ B) = (A “ ran B)
Theorem	dmco 5090	The domain of a composition. Exercise 27 of [Enderton] p. 53. (Contributed by set.mm contributors, 4-Feb-2004.)
⊢ dom (A ∘ B) = (◡B “ dom A)
Theorem	coiun 5091*	Composition with an indexed union. (Contributed by set.mm contributors, 21-Dec-2008.)
⊢ (A ∘ ∪x ∈ C B) = ∪x ∈ C (A ∘ B)
Theorem	cores2 5092	Absorption of a reverse (preimage) restriction of the second member of a class composition. (Contributed by set.mm contributors, 11-Dec-2006.)
⊢ (dom A ⊆ C → (A ∘ ◡(◡B ↾ C)) = (A ∘ B))
Theorem	co02 5093	Composition with the empty set. Theorem 20 of [Suppes] p. 63. (Contributed by set.mm contributors, 24-Apr-2004.)
⊢ (A ∘ ∅) = ∅
Theorem	co01 5094	Composition with the empty set. (Contributed by set.mm contributors, 24-Apr-2004.)
⊢ (∅ ∘ A) = ∅
Theorem	coi1 5095	Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by set.mm contributors, 22-Apr-2004.) (Revised by Scott Fenton, 14-Apr-2021.)
⊢ (A ∘ I ) = A
Theorem	coi2 5096	Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by set.mm contributors, 22-Apr-2004.) (Revised by Scott Fenton, 17-Apr-2021.)
⊢ ( I ∘ A) = A
Theorem	coires1 5097	Composition with a restricted identity relation. (Contributed by FL, 19-Jun-2011.) (Revised by Scott Fenton, 17-Apr-2021.)
⊢ (A ∘ ( I ↾ B)) = (A ↾ B)
Theorem	coass 5098	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 set.mm contributors, 27-Jan-1997.)
⊢ ((A ∘ B) ∘ C) = (A ∘ (B ∘ C))
Theorem	cnvtr 5099	A class is transitive iff its converse is transitive. (Contributed by FL, 19-Sep-2011.) (Revised by Scott Fenton, 18-Apr-2021.)
⊢ ((R ∘ R) ⊆ R ↔ (◡R ∘ ◡R) ⊆ ◡R)
Theorem	ssdmrn 5100	A class is included in the cross product of its domain and range. Exercise 4.12(t) of [Mendelson] p. 235. (Contributed by set.mm contributors, 3-Aug-1994.) (Revised by Scott Fenton, 15-Apr-2021.)
⊢ A ⊆ (dom A × ran A)