Type  Label  Description 
Statement 

Theorem  resopab2 5001* 
Restriction of a class abstraction of ordered pairs. (Contributed by
set.mm contributors, 24Aug2007.)

⊢ (A ⊆ B →
({⟨x,
y⟩ ∣ (x ∈ B ∧ φ)} ↾ A) = {⟨x, y⟩ ∣ (x ∈ A ∧ φ)}) 

Theorem  dfres2 5002* 
Alternate definition of the restriction operation. (Contributed by
Mario Carneiro, 5Nov2013.)

⊢ (R ↾ A) = {⟨x, y⟩ ∣ (x ∈ A ∧ xRy)} 

Theorem  opabresid 5003* 
The restricted identity expressed with the class builder. (Contributed
by FL, 25Apr2012.)

⊢ {⟨x, y⟩ ∣ (x ∈ A ∧ y = x)} = ( I
↾ A) 

Theorem  dmresi 5004 
The domain of a restricted identity function. (Contributed by set.mm
contributors, 27Aug2004.)

⊢ dom ( I ↾
A) = A 

Theorem  resid 5005 
Any class restricted to the universe is itself. (Contributed by set.mm
contributors, 16Mar2004.) (Revised by Scott Fenton, 18Apr2021.)

⊢ (A ↾ V) = A 

Theorem  resima 5006 
A restriction to an image. (Contributed by set.mm contributors,
29Sep2004.)

⊢ ((A ↾ B) “
B) = (A “ B) 

Theorem  resima2 5007 
Image under a restricted class. (Contributed by FL, 31Aug2009.)

⊢ (B ⊆ C →
((A ↾
C) “ B) = (A “
B)) 

Theorem  imadmrn 5008 
The image of the domain of a class is the range of the class.
(Contributed by set.mm contributors, 14Aug1994.)

⊢ (A “
dom A) = ran A 

Theorem  imassrn 5009 
The image of a class is a subset of its range. Theorem 3.16(xi) of
[Monk1] p. 39. (Contributed by set.mm
contributors, 31Mar1995.)

⊢ (A “
B) ⊆
ran A 

Theorem  imai 5010 
Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38.
(Contributed by set.mm contributors, 30Apr1998.)

⊢ ( I “ A) = A 

Theorem  rnresi 5011 
The range of the restricted identity function. (Contributed by set.mm
contributors, 27Aug2004.)

⊢ ran ( I ↾
A) = A 

Theorem  resiima 5012 
The image of a restriction of the identity function. (Contributed by FL,
31Dec2006.)

⊢ (B ⊆ A → ((
I ↾ A)
“ B) = B) 

Theorem  ima0 5013 
Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed
by set.mm contributors, 20May1998.)

⊢ (A “
∅) = ∅ 

Theorem  0ima 5014 
Image under the empty relation. (Contributed by FL, 11Jan2007.)

⊢ (∅ “
A) = ∅ 

Theorem  imadisj 5015 
A class whose image under another is empty is disjoint with the other's
domain. (Contributed by FL, 24Jan2007.)

⊢ ((A “
B) = ∅
↔ (dom A ∩ B) = ∅) 

Theorem  cnvimass 5016 
A preimage under any class is included in the domain of the class.
(Contributed by FL, 29Jan2007.)

⊢ (^{◡}A
“ B) ⊆ dom A 

Theorem  cnvimarndm 5017 
The preimage of the range of a class is the domain of the class.
(Contributed by Jeff Hankins, 15Jul2009.)

⊢ (^{◡}A
“ ran A) = dom A 

Theorem  imasn 5018* 
The image of a singleton. (Contributed by set.mm contributors,
9Jan2015.)

⊢ (R “
{A}) = {y ∣ ARy} 

Theorem  elimasn 5019 
Membership in an image of a singleton. (The proof was shortened by
Andrew Salmon, 27Aug2011.) (Contributed by set.mm contributors,
15Mar2004.) (Revised by set.mm contributors, 27Aug2011.)

⊢ (C ∈ (A “
{B}) ↔ ⟨B, C⟩ ∈ A) 

Theorem  eliniseg 5020 
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, 27Aug2011.) (Contributed by set.mm
contributors, 28Apr2004.) (Revised by set.mm contributors,
27Aug2011.)

⊢ (C ∈ (^{◡}A
“ {B}) ↔ CAB) 

Theorem  epini 5021 
Any set is equal to its preimage under the converse epsilon relation.
(Contributed by Mario Carneiro, 9Mar2013.)

⊢ A ∈ V ⇒ ⊢ (^{◡} E
“ {A}) = A 

Theorem  iniseg 5022* 
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, 28Apr2004.)

⊢ (^{◡}A
“ {B}) = {x ∣ xAB} 

Theorem  imass1 5023 
Subset theorem for image. (Contributed by set.mm contributors,
16Mar2004.)

⊢ (A ⊆ B →
(A “ C) ⊆ (B “ C)) 

Theorem  imass2 5024 
Subset theorem for image. Exercise 22(a) of [Enderton] p. 53.
(Contributed by set.mm contributors, 22Mar1998.)

⊢ (A ⊆ B →
(C “ A) ⊆ (C “ B)) 

Theorem  ndmima 5025 
The image of a singleton outside the domain is empty. (Contributed by
set.mm contributors, 22May1998.)

⊢ (¬ A
∈ dom B
→ (B “ {A}) = ∅) 

Theorem  cotr 5026* 
Two ways of saying a relation is transitive. Definition of transitivity
in [Schechter] p. 51. (The proof was
shortened by Andrew Salmon,
27Aug2011.) (Contributed by set.mm contributors, 27Dec1996.)
(Revised by set.mm contributors, 27Aug2011.)

⊢ ((R ∘ R) ⊆ R ↔
∀x∀y∀z((xRy ∧ yRz) →
xRz)) 

Theorem  cnvsym 5027* 
Two ways of saying a relation is symmetric. Similar to definition of
symmetry in [Schechter] p. 51. (The
proof was shortened by Andrew
Salmon, 27Aug2011.) (Contributed by set.mm contributors,
28Dec1996.) (Revised by set.mm contributors, 27Aug2011.)

⊢ (^{◡}R ⊆ R ↔
∀x∀y(xRy →
yRx)) 

Theorem  intasym 5028* 
Two ways of saying a relation is antisymmetric. Definition of
antisymmetry in [Schechter] p. 51.
(The proof was shortened by Andrew
Salmon, 27Aug2011.) (Contributed by set.mm contributors, 9Sep2004.)
(Revised by set.mm contributors, 27Aug2011.)

⊢ ((R ∩
^{◡}R) ⊆ I ↔
∀x∀y((xRy ∧ yRx) →
x = y)) 

Theorem  intirr 5029* 
Two ways of saying a relation is irreflexive. Definition of
irreflexivity in [Schechter] p. 51.
(Contributed by NM, 9Sep2004.)
(Revised by Andrew Salmon, 27Aug2011.)

⊢ ((R ∩ I
) = ∅ ↔ ∀x ¬
xRx) 

Theorem  cnvopab 5030* 
The converse of a class abstraction of ordered pairs. (The proof was
shortened by Andrew Salmon, 27Aug2011.) (Contributed by set.mm
contributors, 11Dec2003.) (Revised by set.mm contributors,
27Aug2011.)

⊢ ^{◡}{⟨x, y⟩ ∣ φ} =
{⟨y,
x⟩ ∣ φ} 

Theorem  cnv0 5031 
The converse of the empty set. (Contributed by set.mm contributors,
6Apr1998.)

⊢ ^{◡}∅ = ∅ 

Theorem  cnvi 5032 
The converse of the identity relation. Theorem 3.7(ii) of [Monk1]
p. 36. (The proof was shortened by Andrew Salmon, 27Aug2011.)
(Contributed by set.mm contributors, 26Apr1998.) (Revised by set.mm
contributors, 27Aug2011.)

⊢ ^{◡} I =
I 

Theorem  cnvun 5033 
The converse of a union is the union of converses. Theorem 16 of
[Suppes] p. 62. (The proof was shortened
by Andrew Salmon,
27Aug2011.) (Contributed by set.mm contributors, 25Mar1998.)
(Revised by set.mm contributors, 27Aug2011.)

⊢ ^{◡}(A
∪ B) = (^{◡}A ∪
^{◡}B) 

Theorem  cnvdif 5034 
Distributive law for converse over set difference. (Contributed by
set.mm contributors, 26Jun2014.)

⊢ ^{◡}(A
∖ B) =
(^{◡}A ∖ ^{◡}B) 

Theorem  cnvin 5035 
Distributive law for converse over intersection. Theorem 15 of [Suppes]
p. 62. (Contributed by set.mm contributors, 25Mar1998.) (Revised by
set.mm contributors, 26Jun2014.)

⊢ ^{◡}(A
∩ B) = (^{◡}A ∩
^{◡}B) 

Theorem  rnun 5036 
Distributive law for range over union. Theorem 8 of [Suppes] p. 60.
(Contributed by set.mm contributors, 24Mar1998.)

⊢ ran (A
∪ B) = (ran A ∪ ran B) 

Theorem  rnin 5037 
The range of an intersection belongs the intersection of ranges. Theorem
9 of [Suppes] p. 60. (Contributed by
set.mm contributors,
15Sep2004.)

⊢ ran (A
∩ B) ⊆ (ran A
∩ ran B) 

Theorem  rnuni 5038* 
The range of a union. Part of Exercise 8 of [Enderton] p. 41.
(Contributed by set.mm contributors, 17Mar2004.)

⊢ ran ∪A = ∪x ∈ A ran x 

Theorem  imaundi 5039 
Distributive law for image over union. Theorem 35 of [Suppes] p. 65.
(Contributed by set.mm contributors, 30Sep2002.)

⊢ (A “
(B ∪ C)) = ((A
“ B) ∪ (A “ C)) 

Theorem  imaundir 5040 
The image of a union. (Contributed by Jeff Hoffman, 17Feb2008.)

⊢ ((A ∪
B) “ C) = ((A
“ C) ∪ (B “ C)) 

Theorem  dminss 5041 
An upper bound for intersection with a domain. Theorem 40 of [Suppes]
p. 66, who calls it "somewhat surprising." (Contributed by
set.mm
contributors, 11Aug2004.)

⊢ (dom R
∩ A) ⊆ (^{◡}R
“ (R “ A)) 

Theorem  imainss 5042 
An upper bound for intersection with an image. Theorem 41 of [Suppes]
p. 66. (Contributed by set.mm contributors, 11Aug2004.)

⊢ ((R “
A) ∩ B) ⊆ (R “ (A
∩ (^{◡}R “ B))) 

Theorem  cnvxp 5043 
The converse of a cross product. Exercise 11 of [Suppes] p. 67. (The
proof was shortened by Andrew Salmon, 27Aug2011.) (Contributed by
set.mm contributors, 14Aug1999.) (Revised by set.mm contributors,
27Aug2011.)

⊢ ^{◡}(A
× B) = (B × A) 

Theorem  xp0 5044 
The cross product with the empty set is empty. Part of Theorem 3.13(ii)
of [Monk1] p. 37. (Contributed by set.mm
contributors, 12Apr2004.)

⊢ (A ×
∅) = ∅ 

Theorem  xpnz 5045 
The cross product of nonempty classes is nonempty. (Variation of a
theorem contributed by Raph Levien, 30Jun2006.) (Contributed by
set.mm contributors, 30Jun2006.) (Revised by set.mm contributors,
19Apr2007.)

⊢ ((A ≠
∅ ∧
B ≠ ∅) ↔ (A
× B) ≠ ∅) 

Theorem  xpeq0 5046 
At least one member of an empty cross product is empty. (Contributed by
set.mm contributors, 27Aug2006.)

⊢ ((A ×
B) = ∅
↔ (A = ∅ ∨ B = ∅)) 

Theorem  xpdisj1 5047 
Cross products with disjoint sets are disjoint. (Contributed by set.mm
contributors, 13Sep2004.)

⊢ ((A ∩
B) = ∅
→ ((A × C) ∩ (B
× D)) = ∅) 

Theorem  xpdisj2 5048 
Cross products with disjoint sets are disjoint. (Contributed by set.mm
contributors, 13Sep2004.)

⊢ ((A ∩
B) = ∅
→ ((C × A) ∩ (D
× B)) = ∅) 

Theorem  xpsndisj 5049 
Cross products with two different singletons are disjoint. (Contributed
by set.mm contributors, 28Jul2004.) (Revised by set.mm contributors,
3Jun2007.)

⊢ (B ≠
D → ((A × {B})
∩ (C × {D})) = ∅) 

Theorem  resdisj 5050 
A double restriction to disjoint classes is the empty set. (The proof was
shortened by Andrew Salmon, 27Aug2011.) (Contributed by set.mm
contributors, 7Oct2004.) (Revised by set.mm contributors,
27Aug2011.)

⊢ ((A ∩
B) = ∅
→ ((C ↾ A) ↾ B) = ∅) 

Theorem  rnxp 5051 
The range of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37.
(Contributed by set.mm contributors, 12Apr2004.) (Revised by set.mm
contributors, 9Apr2007.)

⊢ (A ≠
∅ → ran (A × B) =
B) 

Theorem  dmxpss 5052 
The domain of a cross product is a subclass of the first factor.
(Contributed by set.mm contributors, 19Mar2007.)

⊢ dom (A
× B) ⊆ A 

Theorem  rnxpss 5053 
The range of a cross product is a subclass of the second factor. (The
proof was shortened by Andrew Salmon, 27Aug2011.) (Contributed by
set.mm contributors, 16Jan2006.) (Revised by set.mm contributors,
27Aug2011.)

⊢ ran (A
× B) ⊆ B 

Theorem  rnxpid 5054 
The range of a square cross product. (Contributed by FL, 17May2010.)

⊢ ran (A
× A) = A 

Theorem  ssxpb 5055 
A crossproduct subclass relationship is equivalent to the relationship
for it components. (Contributed by set.mm contributors, 17Dec2008.)

⊢ ((A ×
B) ≠ ∅ → ((A
× B) ⊆ (C ×
D) ↔ (A ⊆ C ∧ B ⊆ D))) 

Theorem  xp11 5056 
The cross product of nonempty classes is onetoone. (Contributed by
set.mm contributors, 31May2008.)

⊢ ((A ≠
∅ ∧
B ≠ ∅) → ((A
× B) = (C × D)
↔ (A = C ∧ B = D))) 

Theorem  xpcan 5057 
Cancellation law for crossproduct. (Contributed by set.mm contributors,
30Aug2011.)

⊢ (C ≠
∅ → ((C × A) =
(C × B) ↔ A =
B)) 

Theorem  xpcan2 5058 
Cancellation law for crossproduct. (Contributed by set.mm contributors,
30Aug2011.)

⊢ (C ≠
∅ → ((A × C) =
(B × C) ↔ A =
B)) 

Theorem  ssrnres 5059 
Subset of the range of a restriction. (Contributed by set.mm
contributors, 16Jan2006.)

⊢ (B ⊆ ran (C
↾ A)
↔ ran (C ∩ (A × B)) =
B) 

Theorem  rninxp 5060* 
Range of the intersection with a cross product. (The proof was
shortened by Andrew Salmon, 27Aug2011.) (Contributed by set.mm
contributors, 17Jan2006.) (Revised by set.mm contributors,
27Aug2011.)

⊢ (ran (C
∩ (A × B)) = B ↔
∀y
∈ B
∃x
∈ A
xCy) 

Theorem  dminxp 5061* 
Domain of the intersection with a cross product. (Contributed by set.mm
contributors, 17Jan2006.)

⊢ (dom (C
∩ (A × B)) = A ↔
∀x
∈ A
∃y
∈ B
xCy) 

Theorem  cnvcnv 5062 
The double converse of a class is the original class. (Contributed by
Scott Fenton, 17Apr2021.)

⊢ ^{◡}^{◡}R =
R 

Theorem  cnveqb 5063 
Equality theorem for converse. (Contributed by FL, 19Sep2011.)
(Revised by Scott Fenton, 17Apr2021.)

⊢ (A =
B ↔ ^{◡}A =
^{◡}B) 

Theorem  dmsnn0 5064 
The domain of a singleton is nonzero iff the singleton argument is a
set. (Contributed by NM, 14Dec2008.) (Proof shortened by Andrew
Salmon, 27Aug2011.) (Revised by Scott Fenton, 19Apr2021.)

⊢ (A ∈ V ↔ dom {A} ≠ ∅) 

Theorem  rnsnn0 5065 
The range of a singleton is nonzero iff the singleton argument is a set.
(Contributed by set.mm contributors, 14Dec2008.) (Revised by Scott
Fenton, 19Apr2021.)

⊢ (A ∈ V ↔ ran {A} ≠ ∅) 

Theorem  dmsnopg 5066 
The domain of a singleton of an ordered pair is the singleton of the
first member. (Contributed by Mario Carneiro, 26Apr2015.)

⊢ (B ∈ V → dom
{⟨A,
B⟩} =
{A}) 

Theorem  dmsnopss 5067 
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, 30Apr2015.)

⊢ dom {⟨A, B⟩} ⊆ {A} 

Theorem  dmpropg 5068 
The domain of an unordered pair of ordered pairs. (Contributed by Mario
Carneiro, 26Apr2015.)

⊢ ((B ∈ V ∧ D ∈ W) →
dom {⟨A,
B⟩,
⟨C,
D⟩} =
{A, C}) 

Theorem  dmsnop 5069 
The domain of a singleton of an ordered pair is the singleton of the
first member. (Contributed by NM, 30Jan2004.) (Proof shortened by
Andrew Salmon, 27Aug2011.) (Revised by Mario Carneiro,
26Apr2015.)

⊢ B ∈ V ⇒ ⊢ dom {⟨A, B⟩} = {A} 

Theorem  dmprop 5070 
The domain of an unordered pair of ordered pairs. (Contributed by NM,
13Sep2011.)

⊢ B ∈ V
& ⊢ D ∈ V ⇒ ⊢ dom {⟨A, B⟩, ⟨C, D⟩} = {A, C} 

Theorem  dmtpop 5071 
The domain of an unordered triple of ordered pairs. (Contributed by NM,
14Sep2011.)

⊢ B ∈ V
& ⊢ D ∈ V
& ⊢ F ∈ V ⇒ ⊢ dom {⟨A, B⟩, ⟨C, D⟩, ⟨E, F⟩} = {A, C, E} 

Theorem  op1sta 5072 
Extract the first member of an ordered pair. (Contributed by Raph
Levien, 4Dec2003.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ∪dom {⟨A, B⟩} = A 

Theorem  cnvsn 5073 
Converse of a singleton of an ordered pair. (Contributed by NM,
11May1998.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ^{◡}{⟨A, B⟩} = {⟨B, A⟩} 

Theorem  opswap 5074 
Swap the members of an ordered pair. (Contributed by set.mm
contributors, 14Dec2008.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ∪^{◡}{⟨A, B⟩} = ⟨B, A⟩ 

Theorem  rnsnop 5075 
The range of a singleton of an ordered pair is the singleton of the
second member. (Contributed by set.mm contributors, 24Jul2004.)

⊢ A ∈ V ⇒ ⊢ ran {⟨A, B⟩} = {B} 

Theorem  op2nda 5076 
Extract the second member of an ordered pair. (Contributed by set.mm
contributors, 9Jan2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ∪ran {⟨A, B⟩} = B 

Theorem  cnvresima 5077 
An image under the converse of a restriction. (Contributed by Jeff
Hankins, 12Jul2009.)

⊢ (^{◡}(F
↾ A)
“ B) = ((^{◡}F
“ B) ∩ A) 

Theorem  resdmres 5078 
Restriction to the domain of a restriction. (Contributed by set.mm
contributors, 8Apr2007.)

⊢ (A ↾ dom (A
↾ B)) =
(A ↾
B) 

Theorem  imadmres 5079 
The image of the domain of a restriction. (Contributed by set.mm
contributors, 8Apr2007.)

⊢ (A “
dom (A ↾ B)) =
(A “ B) 

Theorem  dfco2 5080* 
Alternate definition of a class composition, using only one bound
variable. (Contributed by set.mm contributors, 19Dec2008.)

⊢ (A ∘ B) =
∪x ∈ V ((^{◡}B
“ {x}) × (A “ {x})) 

Theorem  dfco2a 5081* 
Generalization of dfco2 5080, where C can have any value between
dom A ∩ ran B and V. (The proof was
shortened by Andrew
Salmon, 27Aug2011.) (Contributed by set.mm contributors,
21Dec2008.) (Revised by set.mm contributors, 27Aug2011.)

⊢ ((dom A
∩ ran B) ⊆ C →
(A ∘
B) = ∪x ∈ C ((^{◡}B
“ {x}) × (A “ {x}))) 

Theorem  coundi 5082 
Class composition distributes over union. (The proof was shortened by
Andrew Salmon, 27Aug2011.) (Contributed by set.mm contributors,
21Dec2008.) (Revised by set.mm contributors, 27Aug2011.)

⊢ (A ∘ (B ∪
C)) = ((A ∘ B) ∪ (A
∘ C)) 

Theorem  coundir 5083 
Class composition distributes over union. (The proof was shortened by
Andrew Salmon, 27Aug2011.) (Contributed by set.mm contributors,
21Dec2008.) (Revised by set.mm contributors, 27Aug2011.)

⊢ ((A ∪
B) ∘
C) = ((A ∘ C) ∪ (B
∘ C)) 

Theorem  cores 5084 
Restricted first member of a class composition. (The proof was
shortened by Andrew Salmon, 27Aug2011.) (Contributed by set.mm
contributors, 12Oct2004.) (Revised by set.mm contributors,
27Aug2011.)

⊢ (ran B
⊆ C
→ ((A ↾ C) ∘ B) =
(A ∘
B)) 

Theorem  resco 5085 
Associative law for the restriction of a composition. (Contributed by
set.mm contributors, 12Dec2006.)

⊢ ((A ∘ B) ↾ C) =
(A ∘
(B ↾
C)) 

Theorem  imaco 5086 
Image of the composition of two classes. (Contributed by Jason
Orendorff, 12Dec2006.)

⊢ ((A ∘ B) “
C) = (A “ (B
“ C)) 

Theorem  rnco 5087 
The range of the composition of two classes. (Contributed by set.mm
contributors, 12Dec2006.)

⊢ ran (A
∘ B) =
ran (A ↾ ran B) 

Theorem  rnco2 5088 
The range of the composition of two classes. (Contributed by set.mm
contributors, 27Mar2008.)

⊢ ran (A
∘ B) =
(A “ ran B) 

Theorem  dmco 5089 
The domain of a composition. Exercise 27 of [Enderton] p. 53.
(Contributed by set.mm contributors, 4Feb2004.)

⊢ dom (A
∘ B) =
(^{◡}B “ dom A) 

Theorem  coiun 5090* 
Composition with an indexed union. (Contributed by set.mm contributors,
21Dec2008.)

⊢ (A ∘ ∪x ∈ C B) = ∪x ∈ C (A ∘ B) 

Theorem  cores2 5091 
Absorption of a reverse (preimage) restriction of the second member of a
class composition. (Contributed by set.mm contributors, 11Dec2006.)

⊢ (dom A
⊆ C
→ (A ∘ ^{◡}(^{◡}B ↾ C)) =
(A ∘
B)) 

Theorem  co02 5092 
Composition with the empty set. Theorem 20 of [Suppes] p. 63.
(Contributed by set.mm contributors, 24Apr2004.)

⊢ (A ∘ ∅) = ∅ 

Theorem  co01 5093 
Composition with the empty set. (Contributed by set.mm contributors,
24Apr2004.)

⊢ (∅ ∘ A) = ∅ 

Theorem  coi1 5094 
Composition with the identity relation. Part of Theorem 3.7(i) of
[Monk1] p. 36. (Contributed by set.mm
contributors, 22Apr2004.)
(Revised by Scott Fenton, 14Apr2021.)

⊢ (A ∘ I ) = A 

Theorem  coi2 5095 
Composition with the identity relation. Part of Theorem 3.7(i) of
[Monk1] p. 36. (Contributed by set.mm
contributors, 22Apr2004.)
(Revised by Scott Fenton, 17Apr2021.)

⊢ ( I ∘
A) = A 

Theorem  coires1 5096 
Composition with a restricted identity relation. (Contributed by FL,
19Jun2011.) (Revised by Scott Fenton, 17Apr2021.)

⊢ (A ∘ ( I ↾
B)) = (A ↾ B) 

Theorem  coass 5097 
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, 27Jan1997.)

⊢ ((A ∘ B) ∘ C) =
(A ∘
(B ∘
C)) 

Theorem  cnvtr 5098 
A class is transitive iff its converse is transitive. (Contributed by FL,
19Sep2011.) (Revised by Scott Fenton, 18Apr2021.)

⊢ ((R ∘ R) ⊆ R ↔
(^{◡}R ∘ ^{◡}R)
⊆ ^{◡}R) 

Theorem  ssdmrn 5099 
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, 3Aug1994.) (Revised by Scott Fenton, 15Apr2021.)

⊢ A ⊆ (dom A
× ran A) 

Theorem  dfcnv2 5100 
Definition of converse in terms of image and Swap
. (Contributed by
set.mm contributors, 8Jan2015.)

⊢ ^{◡}A =
( Swap “ A) 