Type  Label  Description 
Statement 

Theorem  ssdmres 5001 
A domain restricted to a subclass equals the subclass. (Contributed by
set.mm contributors, 2Mar1997.) (Revised by set.mm contributors,
28Aug2004.)

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

Theorem  resss 5002 
A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25.
(Contributed by set.mm contributors, 2Aug1994.)

⊢ (A ↾ B) ⊆ A 

Theorem  rescom 5003 
Commutative law for restriction. (Contributed by set.mm contributors,
27Mar1998.)

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

Theorem  ssres 5004 
Subclass theorem for restriction. (Contributed by set.mm contributors,
16Aug1994.)

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

Theorem  ssres2 5005 
Subclass theorem for restriction. (The proof was shortened by Andrew
Salmon, 27Aug2011.) (Contributed by set.mm contributors, 22Mar1998.)
(Revised by set.mm contributors, 27Aug2011.)

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

Theorem  relres 5006 
A restriction is a relation. Exercise 12 of [TakeutiZaring] p. 25. (The
proof was shortened by Andrew Salmon, 27Aug2011.) (Contributed by
set.mm contributors, 2Aug1994.) (Revised by set.mm contributors,
27Aug2011.)

⊢ Rel (A
↾ B) 

Theorem  resabs1 5007 
Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25.
(Contributed by set.mm contributors, 9Aug1994.)

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

Theorem  resabs2 5008 
Absorption law for restriction. (Contributed by set.mm contributors,
27Mar1998.)

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

Theorem  residm 5009 
Idempotent law for restriction. (Contributed by set.mm contributors,
27Mar1998.)

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

Theorem  elres 5010* 
Membership in a restriction. (Contributed by Scott Fenton,
17Mar2011.)

⊢ (A ∈ (B ↾ C) ↔
∃x
∈ C
∃y(A = ⟨x, y⟩ ∧ ⟨x, y⟩ ∈ B)) 

Theorem  elsnres 5011* 
Memebership in restriction to a singleton. (Contributed by Scott
Fenton, 17Mar2011.)

⊢ C ∈ V ⇒ ⊢ (A ∈ (B ↾ {C}) ↔
∃y(A = ⟨C, y⟩ ∧ ⟨C, y⟩ ∈ B)) 

Theorem  relssres 5012 
Simplification law for restriction. (Contributed by set.mm
contributors, 16Aug1994.) (Revised by set.mm contributors,
15Mar2004.)

⊢ ((Rel A
∧ dom A
⊆ B)
→ (A ↾ B) =
A) 

Theorem  resdm 5013 
A relation restricted to its domain equals itself. (Contributed by set.mm
contributors, 12Dec2006.)

⊢ (Rel A
→ (A ↾ dom A) =
A) 

Theorem  resopab 5014* 
Restriction of a class abstraction of ordered pairs. (Contributed by
set.mm contributors, 5Nov2002.)

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

Theorem  iss 5015 
A subclass of the identity function is the identity function restricted
to its domain. (The proof was shortened by Andrew Salmon,
27Aug2011.) (Contributed by set.mm contributors, 13Dec2003.)
(Revised by set.mm contributors, 27Aug2011.)

⊢ (A ⊆ I ↔ A
= ( I ↾ dom A)) 

Theorem  resopab2 5016* 
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 5017* 
Alternate definition of the restriction operation. (Contributed by
Mario Carneiro, 5Nov2013.)

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

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

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

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

⊢ dom ( I ↾
A) = A 

Theorem  resid 5020 
Any relation restricted to the universe is itself. (Contributed by set.mm
contributors, 16Mar2004.)

⊢ (Rel A
→ (A ↾ V) = A) 

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

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

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

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

Theorem  imadmrn 5023 
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 5024 
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 5025 
Image under the identity relation. Theorem 3.16(viii) of [Monk1]
p. 38. (Contributed by set.mm contributors, 30Apr1998.)

⊢ ( I “ A) = A 

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

⊢ ran ( I ↾
A) = A 

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

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

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

⊢ (A “
∅) = ∅ 

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

⊢ (∅ “
A) = ∅ 

Theorem  imadisj 5030 
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 5031 
A preimage under any class is included in the domain of the class.
(Contributed by FL, 29Jan2007.)

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

Theorem  cnvimarndm 5032 
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 5033* 
The image of a singleton. (Contributed by set.mm contributors,
9Jan2015.)

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

Theorem  elimasn 5034 
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 5035 
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 5036 
Any set is equal to its preimage under the converse epsilon relation.
(Contributed by Mario Carneiro, 9Mar2013.)

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

Theorem  iniseg 5037* 
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 5038 
Subset theorem for image. (Contributed by set.mm contributors,
16Mar2004.)

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

Theorem  imass2 5039 
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 5040 
The image of a singleton outside the domain is empty. (Contributed by
set.mm contributors, 22May1998.)

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

Theorem  relcnv 5041 
A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed
by set.mm contributors, 29Oct1996.)

⊢ Rel ^{◡}A 

Theorem  relco 5042 
A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25.
(Contributed by set.mm contributors, 26Jan1997.)

⊢ Rel (A
∘ B) 

Theorem  cotr 5043* 
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 5044* 
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 5045* 
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 5046* 
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 5047* 
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 5048 
The converse of the empty set. (Contributed by set.mm contributors,
6Apr1998.)

⊢ ^{◡}∅ = ∅ 

Theorem  cnvi 5049 
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 5050 
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 5051 
Distributive law for converse over set difference. (Contributed by
set.mm contributors, 26Jun2014.)

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

Theorem  cnvin 5052 
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 5053 
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 5054 
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 5055* 
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 5056 
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 5057 
The image of a union. (Contributed by Jeff Hoffman, 17Feb2008.)

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

Theorem  dminss 5058 
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 5059 
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 5060 
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 5061 
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 5062 
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 5063 
At least one member of an empty cross product is empty. (Contributed by
set.mm contributors, 27Aug2006.)

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

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

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

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

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

Theorem  xpsndisj 5066 
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 5067 
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 5068 
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 5069 
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 5070 
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 5071 
The range of a square cross product. (Contributed by FL, 17May2010.)

⊢ ran (A
× A) = A 

Theorem  ssxpb 5072 
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 5073 
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 5074 
Cancellation law for crossproduct. (Contributed by set.mm contributors,
30Aug2011.)

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

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

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

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

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

Theorem  rninxp 5077* 
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 5078* 
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  dfrel2 5079 
Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25.
(Contributed by set.mm contributors, 29Dec1996.) (Revised by set.mm
contributors, 15Aug2004.)

⊢ (Rel R
↔ ^{◡}^{◡}R =
R) 

Theorem  cnveqb 5080 
Equality theorem for converse. (Contributed by FL, 19Sep2011.)

⊢ ((Rel A
∧ Rel B)
→ (A = B ↔ ^{◡}A =
^{◡}B)) 

Theorem  cnvcnv 5081 
The double converse of a class strips out all elements that are not
ordered pairs. (Contributed by set.mm contributors, 8Dec2003.)

⊢ ^{◡}^{◡}A =
(A ∩ (V × V)) 

Theorem  cnvcnv2 5082 
The double converse of a class equals its restriction to the universe.
(Contributed by set.mm contributors, 8Oct2007.)

⊢ ^{◡}^{◡}A =
(A ↾
V) 

Theorem  cnvcnvss 5083 
The double converse of a class is a subclass. Exercise 2 of
[TakeutiZaring] p. 25. (Contributed
by set.mm contributors,
23Jul2004.)

⊢ ^{◡}^{◡}A ⊆ A 

Theorem  dmsnn0 5084 
The domain of a singleton is nonzero iff the singleton argument is an
ordered pair. (Contributed by NM, 14Dec2008.) (Proof shortened by
Andrew Salmon, 27Aug2011.)

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

Theorem  rnsnn0 5085 
The range of a singleton is nonzero iff the singleton argument is an
ordered pair. (Contributed by set.mm contributors, 14Dec2008.)

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

Theorem  dmsnopg 5086 
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 5087 
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 5088 
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 5089 
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 5090 
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 5091 
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 5092 
Extract the first member of an ordered pair. (Contributed by Raph
Levien, 4Dec2003.)

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

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

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

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

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

Theorem  rnsnop 5095 
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 5096 
Extract the second member of an ordered pair. (Contributed by set.mm
contributors, 9Jan2015.)

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

Theorem  dfrel3 5097 
Alternate definition of relation. (Contributed by set.mm contributors,
14May2008.)

⊢ (Rel R
↔ (R ↾ V) = R) 

Theorem  dmresv 5098 
The domain of a universal restriction. (Contributed by set.mm
contributors, 14May2008.)

⊢ dom (A
↾ V) = dom A 

Theorem  rnresv 5099 
The range of a universal restriction. (Contributed by set.mm
contributors, 14May2008.)

⊢ ran (A
↾ V) = ran A 

Theorem  rescnvcnv 5100 
The restriction of the double converse of a class. (The proof was
shortened by Andrew Salmon, 27Aug2011.) (Contributed by set.mm
contributors, 8Apr2007.) (Revised by set.mm contributors,
27Aug2011.)

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