Type  Label  Description 
Statement 

Theorem  imass2 4701 
Subset theorem for image. Exercise 22(a) of [Enderton] p. 53.
(Contributed by NM, 22Mar1998.)

⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) 

Theorem  ndmima 4702 
The image of a singleton outside the domain is empty. (Contributed by NM,
22May1998.)

⊢ (¬ 𝐴 ∈ dom 𝐵 → (𝐵 “ {𝐴}) = ∅) 

Theorem  relcnv 4703 
A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed
by NM, 29Oct1996.)

⊢ Rel ^{◡}𝐴 

Theorem  relbrcnvg 4704 
When 𝑅 is a relation, the sethood
assumptions on brcnv 4518 can be
omitted. (Contributed by Mario Carneiro, 28Apr2015.)

⊢ (Rel 𝑅 → (𝐴^{◡}𝑅𝐵 ↔ 𝐵𝑅𝐴)) 

Theorem  relbrcnv 4705 
When 𝑅 is a relation, the sethood
assumptions on brcnv 4518 can be
omitted. (Contributed by Mario Carneiro, 28Apr2015.)

⊢ Rel 𝑅 ⇒ ⊢ (𝐴^{◡}𝑅𝐵 ↔ 𝐵𝑅𝐴) 

Theorem  cotr 4706* 
Two ways of saying a relation is transitive. Definition of transitivity
in [Schechter] p. 51. (Contributed by
NM, 27Dec1996.) (Proof
shortened by Andrew Salmon, 27Aug2011.)

⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) 

Theorem  issref 4707* 
Two ways to state a relation is reflexive. Adapted from Tarski.
(Contributed by FL, 15Jan2012.) (Revised by NM, 30Mar2016.)

⊢ (( I ↾ 𝐴) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥) 

Theorem  cnvsym 4708* 
Two ways of saying a relation is symmetric. Similar to definition of
symmetry in [Schechter] p. 51.
(Contributed by NM, 28Dec1996.)
(Proof shortened by Andrew Salmon, 27Aug2011.)

⊢ (^{◡}𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) 

Theorem  intasym 4709* 
Two ways of saying a relation is antisymmetric. Definition of
antisymmetry in [Schechter] p. 51.
(Contributed by NM, 9Sep2004.)
(Proof shortened by Andrew Salmon, 27Aug2011.)

⊢ ((𝑅 ∩ ^{◡}𝑅) ⊆ I ↔ ∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) 

Theorem  asymref 4710* 
Two ways of saying a relation is antisymmetric and reflexive.
∪ ∪ 𝑅 is the field of a relation by relfld 4846. (Contributed by
NM, 6May2008.) (Proof shortened by Andrew Salmon, 27Aug2011.)

⊢ ((𝑅 ∩ ^{◡}𝑅) = ( I ↾ ∪ ∪ 𝑅) ↔ ∀𝑥 ∈ ∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦)) 

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

⊢ ((𝑅 ∩ I ) = ∅ ↔ ∀𝑥 ¬ 𝑥𝑅𝑥) 

Theorem  brcodir 4712* 
Two ways of saying that two elements have an upper bound. (Contributed
by Mario Carneiro, 3Nov2015.)

⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(^{◡}𝑅 ∘ 𝑅)𝐵 ↔ ∃𝑧(𝐴𝑅𝑧 ∧ 𝐵𝑅𝑧))) 

Theorem  codir 4713* 
Two ways of saying a relation is directed. (Contributed by Mario
Carneiro, 22Nov2013.)

⊢ ((𝐴 × 𝐵) ⊆ (^{◡}𝑅 ∘ 𝑅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∃𝑧(𝑥𝑅𝑧 ∧ 𝑦𝑅𝑧)) 

Theorem  qfto 4714* 
A quantifierfree way of expressing the total order predicate.
(Contributed by Mario Carneiro, 22Nov2013.)

⊢ ((𝐴 × 𝐵) ⊆ (𝑅 ∪ ^{◡}𝑅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥)) 

Theorem  xpidtr 4715 
A square cross product (𝐴 × 𝐴) is a transitive relation.
(Contributed by FL, 31Jul2009.)

⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) 

Theorem  trin2 4716 
The intersection of two transitive classes is transitive. (Contributed
by FL, 31Jul2009.)

⊢ (((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ((𝑅 ∩ 𝑆) ∘ (𝑅 ∩ 𝑆)) ⊆ (𝑅 ∩ 𝑆)) 

Theorem  poirr2 4717 
A partial order relation is irreflexive. (Contributed by Mario
Carneiro, 2Nov2015.)

⊢ (𝑅 Po 𝐴 → (𝑅 ∩ ( I ↾ 𝐴)) = ∅) 

Theorem  trinxp 4718 
The relation induced by a transitive relation on a part of its field is
transitive. (Taking the intersection of a relation with a square cross
product is a way to restrict it to a subset of its field.) (Contributed
by FL, 31Jul2009.)

⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ (𝑅 ∩ (𝐴 × 𝐴))) 

Theorem  soirri 4719 
A strict order relation is irreflexive. (Contributed by NM,
10Feb1996.) (Revised by Mario Carneiro, 10May2013.)

⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ¬ 𝐴𝑅𝐴 

Theorem  sotri 4720 
A strict order relation is a transitive relation. (Contributed by NM,
10Feb1996.) (Revised by Mario Carneiro, 10May2013.)

⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) 

Theorem  son2lpi 4721 
A strict order relation has no 2cycle loops. (Contributed by NM,
10Feb1996.) (Revised by Mario Carneiro, 10May2013.)

⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ¬ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) 

Theorem  sotri2 4722 
A transitivity relation. (Read ¬ B < A and B
< C implies A <
C .) (Contributed by Mario Carneiro, 10May2013.)

⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ ¬ 𝐵𝑅𝐴 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) 

Theorem  sotri3 4723 
A transitivity relation. (Read A < B and ¬ C
< B implies A <
C .) (Contributed by Mario Carneiro, 10May2013.)

⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐴𝑅𝐵 ∧ ¬ 𝐶𝑅𝐵) → 𝐴𝑅𝐶) 

Theorem  poleloe 4724 
Express "less than or equals" for general strict orders.
(Contributed by
Stefan O'Rear, 17Jan2015.)

⊢ (𝐵 ∈ 𝑉 → (𝐴(𝑅 ∪ I )𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵))) 

Theorem  poltletr 4725 
Transitive law for general strict orders. (Contributed by Stefan O'Rear,
17Jan2015.)

⊢ ((𝑅 Po 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑅𝐵 ∧ 𝐵(𝑅 ∪ I )𝐶) → 𝐴𝑅𝐶)) 

Theorem  cnvopab 4726* 
The converse of a class abstraction of ordered pairs. (Contributed by
NM, 11Dec2003.) (Proof shortened by Andrew Salmon, 27Aug2011.)

⊢ ^{◡}{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑦, 𝑥⟩ ∣ 𝜑} 

Theorem  cnv0 4727 
The converse of the empty set. (Contributed by NM, 6Apr1998.)

⊢ ^{◡}∅ = ∅ 

Theorem  cnvi 4728 
The converse of the identity relation. Theorem 3.7(ii) of [Monk1]
p. 36. (Contributed by NM, 26Apr1998.) (Proof shortened by Andrew
Salmon, 27Aug2011.)

⊢ ^{◡} I
= I 

Theorem  cnvun 4729 
The converse of a union is the union of converses. Theorem 16 of
[Suppes] p. 62. (Contributed by NM,
25Mar1998.) (Proof shortened by
Andrew Salmon, 27Aug2011.)

⊢ ^{◡}(𝐴 ∪ 𝐵) = (^{◡}𝐴 ∪ ^{◡}𝐵) 

Theorem  cnvdif 4730 
Distributive law for converse over set difference. (Contributed by
Mario Carneiro, 26Jun2014.)

⊢ ^{◡}(𝐴 ∖ 𝐵) = (^{◡}𝐴 ∖ ^{◡}𝐵) 

Theorem  cnvin 4731 
Distributive law for converse over intersection. Theorem 15 of [Suppes]
p. 62. (Contributed by NM, 25Mar1998.) (Revised by Mario Carneiro,
26Jun2014.)

⊢ ^{◡}(𝐴 ∩ 𝐵) = (^{◡}𝐴 ∩ ^{◡}𝐵) 

Theorem  rnun 4732 
Distributive law for range over union. Theorem 8 of [Suppes] p. 60.
(Contributed by NM, 24Mar1998.)

⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵) 

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

⊢ ran (𝐴 ∩ 𝐵) ⊆ (ran 𝐴 ∩ ran 𝐵) 

Theorem  rniun 4734 
The range of an indexed union. (Contributed by Mario Carneiro,
29May2015.)

⊢ ran ∪
𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 ran 𝐵 

Theorem  rnuni 4735* 
The range of a union. Part of Exercise 8 of [Enderton] p. 41.
(Contributed by NM, 17Mar2004.) (Revised by Mario Carneiro,
29May2015.)

⊢ ran ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ran 𝑥 

Theorem  imaundi 4736 
Distributive law for image over union. Theorem 35 of [Suppes] p. 65.
(Contributed by NM, 30Sep2002.)

⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) 

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

⊢ ((𝐴 ∪ 𝐵) “ 𝐶) = ((𝐴 “ 𝐶) ∪ (𝐵 “ 𝐶)) 

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

⊢ (dom 𝑅 ∩ 𝐴) ⊆ (^{◡}𝑅 “ (𝑅 “ 𝐴)) 

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

⊢ ((𝑅 “ 𝐴) ∩ 𝐵) ⊆ (𝑅 “ (𝐴 ∩ (^{◡}𝑅 “ 𝐵))) 

Theorem  inimass 4740 
The image of an intersection (Contributed by Thierry Arnoux,
16Dec2017.)

⊢ ((𝐴 ∩ 𝐵) “ 𝐶) ⊆ ((𝐴 “ 𝐶) ∩ (𝐵 “ 𝐶)) 

Theorem  inimasn 4741 
The intersection of the image of singleton (Contributed by Thierry
Arnoux, 16Dec2017.)

⊢ (𝐶 ∈ 𝑉 → ((𝐴 ∩ 𝐵) “ {𝐶}) = ((𝐴 “ {𝐶}) ∩ (𝐵 “ {𝐶}))) 

Theorem  cnvxp 4742 
The converse of a cross product. Exercise 11 of [Suppes] p. 67.
(Contributed by NM, 14Aug1999.) (Proof shortened by Andrew Salmon,
27Aug2011.)

⊢ ^{◡}(𝐴 × 𝐵) = (𝐵 × 𝐴) 

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

⊢ (𝐴 × ∅) =
∅ 

Theorem  xpmlem 4744* 
The cross product of inhabited classes is inhabited. (Contributed by
Jim Kingdon, 11Dec2018.)

⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) ↔ ∃𝑧 𝑧 ∈ (𝐴 × 𝐵)) 

Theorem  xpm 4745* 
The cross product of inhabited classes is inhabited. (Contributed by
Jim Kingdon, 13Dec2018.)

⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) ↔ ∃𝑧 𝑧 ∈ (𝐴 × 𝐵)) 

Theorem  xpeq0r 4746 
A cross product is empty if at least one member is empty. (Contributed by
Jim Kingdon, 12Dec2018.)

⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅) 

Theorem  xpdisj1 4747 
Cross products with disjoint sets are disjoint. (Contributed by NM,
13Sep2004.)

⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 × 𝐶) ∩ (𝐵 × 𝐷)) = ∅) 

Theorem  xpdisj2 4748 
Cross products with disjoint sets are disjoint. (Contributed by NM,
13Sep2004.)

⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 × 𝐴) ∩ (𝐷 × 𝐵)) = ∅) 

Theorem  xpsndisj 4749 
Cross products with two different singletons are disjoint. (Contributed
by NM, 28Jul2004.)

⊢ (𝐵 ≠ 𝐷 → ((𝐴 × {𝐵}) ∩ (𝐶 × {𝐷})) = ∅) 

Theorem  djudisj 4750* 
Disjoint unions with disjoint index sets are disjoint. (Contributed by
Stefan O'Rear, 21Nov2014.)

⊢ ((𝐴 ∩ 𝐵) = ∅ → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐶) ∩ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝐷)) = ∅) 

Theorem  resdisj 4751 
A double restriction to disjoint classes is the empty set. (Contributed
by NM, 7Oct2004.) (Proof shortened by Andrew Salmon, 27Aug2011.)

⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 ↾ 𝐴) ↾ 𝐵) = ∅) 

Theorem  rnxpm 4752* 
The range of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37,
with nonempty changed to inhabited. (Contributed by Jim Kingdon,
12Dec2018.)

⊢ (∃𝑥 𝑥 ∈ 𝐴 → ran (𝐴 × 𝐵) = 𝐵) 

Theorem  dmxpss 4753 
The domain of a cross product is a subclass of the first factor.
(Contributed by NM, 19Mar2007.)

⊢ dom (𝐴 × 𝐵) ⊆ 𝐴 

Theorem  rnxpss 4754 
The range of a cross product is a subclass of the second factor.
(Contributed by NM, 16Jan2006.) (Proof shortened by Andrew Salmon,
27Aug2011.)

⊢ ran (𝐴 × 𝐵) ⊆ 𝐵 

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

⊢ ran (𝐴 × 𝐴) = 𝐴 

Theorem  ssxpbm 4756* 
A crossproduct subclass relationship is equivalent to the relationship
for its components. (Contributed by Jim Kingdon, 12Dec2018.)

⊢ (∃𝑥 𝑥 ∈ (𝐴 × 𝐵) → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷))) 

Theorem  ssxp1 4757* 
Cross product subset cancellation. (Contributed by Jim Kingdon,
14Dec2018.)

⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐴 × 𝐶) ⊆ (𝐵 × 𝐶) ↔ 𝐴 ⊆ 𝐵)) 

Theorem  ssxp2 4758* 
Cross product subset cancellation. (Contributed by Jim Kingdon,
14Dec2018.)

⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐶 × 𝐴) ⊆ (𝐶 × 𝐵) ↔ 𝐴 ⊆ 𝐵)) 

Theorem  xp11m 4759* 
The cross product of inhabited classes is onetoone. (Contributed by
Jim Kingdon, 13Dec2018.)

⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) → ((𝐴 × 𝐵) = (𝐶 × 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) 

Theorem  xpcanm 4760* 
Cancellation law for crossproduct. (Contributed by Jim Kingdon,
14Dec2018.)

⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐶 × 𝐴) = (𝐶 × 𝐵) ↔ 𝐴 = 𝐵)) 

Theorem  xpcan2m 4761* 
Cancellation law for crossproduct. (Contributed by Jim Kingdon,
14Dec2018.)

⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐴 × 𝐶) = (𝐵 × 𝐶) ↔ 𝐴 = 𝐵)) 

Theorem  xpexr2m 4762* 
If a nonempty cross product is a set, so are both of its components.
(Contributed by Jim Kingdon, 14Dec2018.)

⊢ (((𝐴 × 𝐵) ∈ 𝐶 ∧ ∃𝑥 𝑥 ∈ (𝐴 × 𝐵)) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) 

Theorem  ssrnres 4763 
Subset of the range of a restriction. (Contributed by NM,
16Jan2006.)

⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) ↔ ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵) 

Theorem  rninxp 4764* 
Range of the intersection with a cross product. (Contributed by NM,
17Jan2006.) (Proof shortened by Andrew Salmon, 27Aug2011.)

⊢ (ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐶𝑦) 

Theorem  dminxp 4765* 
Domain of the intersection with a cross product. (Contributed by NM,
17Jan2006.)

⊢ (dom (𝐶 ∩ (𝐴 × 𝐵)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥𝐶𝑦) 

Theorem  imainrect 4766 
Image of a relation restricted to a rectangular region. (Contributed by
Stefan O'Rear, 19Feb2015.)

⊢ ((𝐺 ∩ (𝐴 × 𝐵)) “ 𝑌) = ((𝐺 “ (𝑌 ∩ 𝐴)) ∩ 𝐵) 

Theorem  xpima1 4767 
The image by a cross product. (Contributed by Thierry Arnoux,
16Dec2017.)

⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) “ 𝐶) = ∅) 

Theorem  xpima2m 4768* 
The image by a cross product. (Contributed by Thierry Arnoux,
16Dec2017.)

⊢ (∃𝑥 𝑥 ∈ (𝐴 ∩ 𝐶) → ((𝐴 × 𝐵) “ 𝐶) = 𝐵) 

Theorem  xpimasn 4769 
The image of a singleton by a cross product. (Contributed by Thierry
Arnoux, 14Jan2018.)

⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵) 

Theorem  cnvcnv3 4770* 
The set of all ordered pairs in a class is the same as the double
converse. (Contributed by Mario Carneiro, 16Aug2015.)

⊢ ^{◡}^{◡}𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦} 

Theorem  dfrel2 4771 
Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25.
(Contributed by NM, 29Dec1996.)

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

Theorem  dfrel4v 4772* 
A relation can be expressed as the set of ordered pairs in it.
(Contributed by Mario Carneiro, 16Aug2015.)

⊢ (Rel 𝑅 ↔ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦}) 

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

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

Theorem  cnvcnv2 4774 
The double converse of a class equals its restriction to the universe.
(Contributed by NM, 8Oct2007.)

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

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

⊢ ^{◡}^{◡}𝐴 ⊆ 𝐴 

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

⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ^{◡}𝐴 = ^{◡}𝐵)) 

Theorem  cnveq0 4777 
A relation empty iff its converse is empty. (Contributed by FL,
19Sep2011.)

⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ^{◡}𝐴 = ∅)) 

Theorem  dfrel3 4778 
Alternate definition of relation. (Contributed by NM, 14May2008.)

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

Theorem  dmresv 4779 
The domain of a universal restriction. (Contributed by NM,
14May2008.)

⊢ dom (𝐴 ↾ V) = dom 𝐴 

Theorem  rnresv 4780 
The range of a universal restriction. (Contributed by NM,
14May2008.)

⊢ ran (𝐴 ↾ V) = ran 𝐴 

Theorem  dfrn4 4781 
Range defined in terms of image. (Contributed by NM, 14May2008.)

⊢ ran 𝐴 = (𝐴 “ V) 

Theorem  csbrng 4782 
Distribute proper substitution through the range of a class.
(Contributed by Alan Sare, 10Nov2012.)

⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵) 

Theorem  rescnvcnv 4783 
The restriction of the double converse of a class. (Contributed by NM,
8Apr2007.) (Proof shortened by Andrew Salmon, 27Aug2011.)

⊢ (^{◡}^{◡}𝐴 ↾ 𝐵) = (𝐴 ↾ 𝐵) 

Theorem  cnvcnvres 4784 
The double converse of the restriction of a class. (Contributed by NM,
3Jun2007.)

⊢ ^{◡}^{◡}(𝐴 ↾ 𝐵) = (^{◡}^{◡}𝐴 ↾ 𝐵) 

Theorem  imacnvcnv 4785 
The image of the double converse of a class. (Contributed by NM,
8Apr2007.)

⊢ (^{◡}^{◡}𝐴 “ 𝐵) = (𝐴 “ 𝐵) 

Theorem  dmsnm 4786* 
The domain of a singleton is inhabited iff the singleton argument is an
ordered pair. (Contributed by Jim Kingdon, 15Dec2018.)

⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥 𝑥 ∈ dom {𝐴}) 

Theorem  rnsnm 4787* 
The range of a singleton is inhabited iff the singleton argument is an
ordered pair. (Contributed by Jim Kingdon, 15Dec2018.)

⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥 𝑥 ∈ ran {𝐴}) 

Theorem  dmsn0 4788 
The domain of the singleton of the empty set is empty. (Contributed by
NM, 30Jan2004.)

⊢ dom {∅} = ∅ 

Theorem  cnvsn0 4789 
The converse of the singleton of the empty set is empty. (Contributed by
Mario Carneiro, 30Aug2015.)

⊢ ^{◡}{∅} = ∅ 

Theorem  dmsn0el 4790 
The domain of a singleton is empty if the singleton's argument contains
the empty set. (Contributed by NM, 15Dec2008.)

⊢ (∅ ∈ 𝐴 → dom {𝐴} = ∅) 

Theorem  relsn2m 4791* 
A singleton is a relation iff it has an inhabited domain. (Contributed
by Jim Kingdon, 16Dec2018.)

⊢ 𝐴 ∈ V ⇒ ⊢ (Rel {𝐴} ↔ ∃𝑥 𝑥 ∈ dom {𝐴}) 

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

⊢ (𝐵 ∈ 𝑉 → dom {⟨𝐴, 𝐵⟩} = {𝐴}) 

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

⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {𝐴, 𝐶}) 

Theorem  dmsnop 4794 
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.)

⊢ 𝐵 ∈ V ⇒ ⊢ dom {⟨𝐴, 𝐵⟩} = {𝐴} 

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

⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈
V ⇒ ⊢ dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {𝐴, 𝐶} 

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

⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐹 ∈
V ⇒ ⊢ dom {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩} = {𝐴, 𝐶, 𝐸} 

Theorem  cnvcnvsn 4797 
Double converse of a singleton of an ordered pair. (Unlike cnvsn 4803,
this does not need any sethood assumptions on 𝐴 and 𝐵.)
(Contributed by Mario Carneiro, 26Apr2015.)

⊢ ^{◡}^{◡}{⟨𝐴, 𝐵⟩} = ^{◡}{⟨𝐵, 𝐴⟩} 

Theorem  dmsnsnsng 4798 
The domain of the singleton of the singleton of a singleton.
(Contributed by Jim Kingdon, 16Dec2018.)

⊢ (𝐴 ∈ V → dom {{{𝐴}}} = {𝐴}) 

Theorem  rnsnopg 4799 
The range of a singleton of an ordered pair is the singleton of the second
member. (Contributed by NM, 24Jul2004.) (Revised by Mario Carneiro,
30Apr2015.)

⊢ (𝐴 ∈ 𝑉 → ran {⟨𝐴, 𝐵⟩} = {𝐵}) 

Theorem  rnpropg 4800 
The range of a pair of ordered pairs is the pair of second members.
(Contributed by Thierry Arnoux, 3Jan2017.)

⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} = {𝐶, 𝐷}) 