Type  Label  Description 
Statement 

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

⊢ (∃x x ∈ 𝐶 → ((𝐶 × A) ⊆ (𝐶 × B) ↔ A
⊆ B)) 

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

⊢ ((∃x x ∈ A ∧ ∃y y ∈ B) →
((A × B) = (𝐶 × 𝐷) ↔ (A = 𝐶 ∧
B = 𝐷))) 

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

⊢ (∃x x ∈ 𝐶 → ((𝐶 × A) = (𝐶 × B) ↔ A =
B)) 

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

⊢ (∃x x ∈ 𝐶 → ((A × 𝐶) = (B
× 𝐶) ↔ A = B)) 

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

⊢ (((A
× B) ∈ 𝐶 ∧ ∃x x ∈ (A × B))
→ (A ∈ V ∧ B ∈
V)) 

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

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

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

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

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

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

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

⊢ ((𝐺 ∩ (A × B))
“ 𝑌) = ((𝐺 “ (𝑌 ∩ A)) ∩ B) 

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

⊢ ((A ∩
𝐶) = ∅ →
((A × B) “ 𝐶) = ∅) 

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

⊢ (∃x x ∈ (A ∩
𝐶) → ((A × B)
“ 𝐶) = B) 

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

⊢ (𝑋 ∈
A → ((A × B)
“ {𝑋}) = B) 

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

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

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

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

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

⊢ (Rel 𝑅 ↔ 𝑅 = {⟨x, y⟩
∣ x𝑅y}) 

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ dom (A
↾ V) = dom A 

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

⊢ ran (A
↾ V) = ran A 

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

⊢ ran A =
(A “ V) 

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

⊢ (A ∈ 𝑉 → ⦋A / x⦌ran B = ran ⦋A / x⦌B) 

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

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

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

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

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

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

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

⊢ (A ∈ (V × V) ↔ ∃x x ∈ dom {A}) 

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

⊢ (A ∈ (V × V) ↔ ∃x x ∈ ran {A}) 

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

⊢ dom {∅} = ∅ 

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

⊢ ^{◡}{∅} = ∅ 

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

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

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

⊢ A ∈ V ⇒ ⊢ (Rel {A} ↔ ∃x x ∈ dom {A}) 

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

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

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

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

Theorem  dmsnop 4737 
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 4738 
The domain of an unordered pair of ordered pairs. (Contributed by NM,
13Sep2011.)

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

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

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

Theorem  cnvcnvsn 4740 
Double converse of a singleton of an ordered pair. (Unlike cnvsn 4746,
this does not need any sethood assumptions on A and B.)
(Contributed by Mario Carneiro, 26Apr2015.)

⊢ ^{◡}^{◡}{⟨A, B⟩} =
^{◡}{⟨B, A⟩} 

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

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

Theorem  rnsnopg 4742 
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.)

⊢ (A ∈ 𝑉 → ran {⟨A, B⟩} =
{B}) 

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

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

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

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

Theorem  op1sta 4745 
Extract the first member of an ordered pair. (See op2nda 4748 to extract
the second member and op1stb 4175 for an alternate version.)
(Contributed
by Raph Levien, 4Dec2003.)

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

Theorem  cnvsn 4746 
Converse of a singleton of an ordered pair. (Contributed by NM,
11May1998.) (Revised by Mario Carneiro, 26Apr2015.)

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

Theorem  op2ndb 4747 
Extract the second member of an ordered pair. Theorem 5.12(ii) of
[Monk1] p. 52. (See op1stb 4175 to extract the first member and op2nda 4748
for an alternate version.) (Contributed by NM, 25Nov2003.)

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

Theorem  op2nda 4748 
Extract the second member of an ordered pair. (See op1sta 4745 to extract
the first member and op2ndb 4747 for an alternate version.) (Contributed
by NM, 17Feb2004.) (Proof shortened by Andrew Salmon,
27Aug2011.)

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

Theorem  cnvsng 4749 
Converse of a singleton of an ordered pair. (Contributed by NM,
23Jan2015.)

⊢ ((A ∈ 𝑉 ∧
B ∈
𝑊) → ^{◡}{⟨A, B⟩} =
{⟨B, A⟩}) 

Theorem  opswapg 4750 
Swap the members of an ordered pair. (Contributed by Jim Kingdon,
16Dec2018.)

⊢ ((A ∈ 𝑉 ∧
B ∈
𝑊) → ∪ ^{◡}{⟨A, B⟩} =
⟨B, A⟩) 

Theorem  elxp4 4751 
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp5 4752. (Contributed by NM,
17Feb2004.)

⊢ (A ∈ (B ×
𝐶) ↔ (A = ⟨∪ dom
{A}, ∪ ran
{A}⟩ ∧ (∪ dom {A} ∈ B ∧ ∪ ran {A} ∈ 𝐶))) 

Theorem  elxp5 4752 
Membership in a cross product requiring no quantifiers or dummy
variables. Provides a slightly shorter version of elxp4 4751 when the
double intersection does not create class existence problems (caused by
int0 3620). (Contributed by NM, 1Aug2004.)

⊢ (A ∈ (B ×
𝐶) ↔ (A = ⟨∩ ∩ A, ∪ ran {A}⟩ ∧ (∩ ∩ A ∈ B ∧ ∪ ran {A} ∈ 𝐶))) 

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

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

Theorem  resdm2 4754 
A class restricted to its domain equals its double converse. (Contributed
by NM, 8Apr2007.)

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

Theorem  resdmres 4755 
Restriction to the domain of a restriction. (Contributed by NM,
8Apr2007.)

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

Theorem  imadmres 4756 
The image of the domain of a restriction. (Contributed by NM,
8Apr2007.)

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

Theorem  mptpreima 4757* 
The preimage of a function in mapsto notation. (Contributed by Stefan
O'Rear, 25Jan2015.)

⊢ 𝐹 = (x
∈ A
↦ B) ⇒ ⊢ (^{◡}𝐹 “ 𝐶) = {x
∈ A
∣ B ∈ 𝐶} 

Theorem  mptiniseg 4758* 
Converse singleton image of a function defined by mapsto. (Contributed
by Stefan O'Rear, 25Jan2015.)

⊢ 𝐹 = (x
∈ A
↦ B) ⇒ ⊢ (𝐶 ∈ 𝑉 → (^{◡}𝐹 “ {𝐶}) = {x
∈ A
∣ B = 𝐶}) 

Theorem  dmmpt 4759 
The domain of the mapping operation in general. (Contributed by NM,
16May1995.) (Revised by Mario Carneiro, 22Mar2015.)

⊢ 𝐹 = (x
∈ A
↦ B) ⇒ ⊢ dom 𝐹 = {x
∈ A
∣ B ∈ V} 

Theorem  dmmptss 4760* 
The domain of a mapping is a subset of its base class. (Contributed by
Scott Fenton, 17Jun2013.)

⊢ 𝐹 = (x
∈ A
↦ B) ⇒ ⊢ dom 𝐹 ⊆ A 

Theorem  dmmptg 4761* 
The domain of the mapping operation is the stated domain, if the
function value is always a set. (Contributed by Mario Carneiro,
9Feb2013.) (Revised by Mario Carneiro, 14Sep2013.)

⊢ (∀x ∈ A B ∈ 𝑉 → dom (x ∈ A ↦ B) =
A) 

Theorem  relco 4762 
A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25.
(Contributed by NM, 26Jan1997.)

⊢ Rel (A
∘ B) 

Theorem  dfco2 4763* 
Alternate definition of a class composition, using only one bound
variable. (Contributed by NM, 19Dec2008.)

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

Theorem  dfco2a 4764* 
Generalization of dfco2 4763, where 𝐶 can have any value between
dom A ∩ ran
B and V.
(Contributed by NM, 21Dec2008.)
(Proof shortened by Andrew Salmon, 27Aug2011.)

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

Theorem  coundi 4765 
Class composition distributes over union. (Contributed by NM,
21Dec2008.) (Proof shortened by Andrew Salmon, 27Aug2011.)

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

Theorem  coundir 4766 
Class composition distributes over union. (Contributed by NM,
21Dec2008.) (Proof shortened by Andrew Salmon, 27Aug2011.)

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

Theorem  cores 4767 
Restricted first member of a class composition. (Contributed by NM,
12Oct2004.) (Proof shortened by Andrew Salmon, 27Aug2011.)

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

Theorem  resco 4768 
Associative law for the restriction of a composition. (Contributed by
NM, 12Dec2006.)

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

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

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

Theorem  rnco 4770 
The range of the composition of two classes. (Contributed by NM,
12Dec2006.)

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

Theorem  rnco2 4771 
The range of the composition of two classes. (Contributed by NM,
27Mar2008.)

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

Theorem  dmco 4772 
The domain of a composition. Exercise 27 of [Enderton] p. 53.
(Contributed by NM, 4Feb2004.)

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

Theorem  coiun 4773* 
Composition with an indexed union. (Contributed by NM, 21Dec2008.)

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

Theorem  cocnvcnv1 4774 
A composition is not affected by a double converse of its first argument.
(Contributed by NM, 8Oct2007.)

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

Theorem  cocnvcnv2 4775 
A composition is not affected by a double converse of its second
argument. (Contributed by NM, 8Oct2007.)

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

Theorem  cores2 4776 
Absorption of a reverse (preimage) restriction of the second member of a
class composition. (Contributed by NM, 11Dec2006.)

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

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

⊢ (A ∘
∅) = ∅ 

Theorem  co01 4778 
Composition with the empty set. (Contributed by NM, 24Apr2004.)

⊢ (∅ ∘ A) = ∅ 

Theorem  coi1 4779 
Composition with the identity relation. Part of Theorem 3.7(i) of
[Monk1] p. 36. (Contributed by NM,
22Apr2004.)

⊢ (Rel A
→ (A ∘ I ) = A) 

Theorem  coi2 4780 
Composition with the identity relation. Part of Theorem 3.7(i) of
[Monk1] p. 36. (Contributed by NM,
22Apr2004.)

⊢ (Rel A
→ ( I ∘ A) = A) 

Theorem  coires1 4781 
Composition with a restricted identity relation. (Contributed by FL,
19Jun2011.) (Revised by Stefan O'Rear, 7Mar2015.)

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

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

⊢ ((A ∘
B) ∘ 𝐶) = (A
∘ (B ∘ 𝐶)) 

Theorem  relcnvtr 4783 
A relation is transitive iff its converse is transitive. (Contributed by
FL, 19Sep2011.)

⊢ (Rel 𝑅 → ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ (^{◡}𝑅 ∘ ^{◡}𝑅) ⊆ ^{◡}𝑅)) 

Theorem  relssdmrn 4784 
A relation is included in the cross product of its domain and range.
Exercise 4.12(t) of [Mendelson] p.
235. (Contributed by NM,
3Aug1994.)

⊢ (Rel A
→ A ⊆ (dom A × ran A)) 

Theorem  cnvssrndm 4785 
The converse is a subset of the cartesian product of range and domain.
(Contributed by Mario Carneiro, 2Jan2017.)

⊢ ^{◡}A
⊆ (ran A × dom A) 

Theorem  cossxp 4786 
Composition as a subset of the cross product of factors. (Contributed by
Mario Carneiro, 12Jan2017.)

⊢ (A ∘
B) ⊆ (dom B × ran A) 

Theorem  relrelss 4787 
Two ways to describe the structure of a twoplace operation. (Contributed
by NM, 17Dec2008.)

⊢ ((Rel A
∧ Rel dom A) ↔ A
⊆ ((V × V) × V)) 

Theorem  unielrel 4788 
The membership relation for a relation is inherited by class union.
(Contributed by NM, 17Sep2006.)

⊢ ((Rel 𝑅 ∧
A ∈
𝑅) → ∪ A ∈ ∪ 𝑅) 

Theorem  relfld 4789 
The double union of a relation is its field. (Contributed by NM,
17Sep2006.)

⊢ (Rel 𝑅 → ∪ ∪ 𝑅 =
(dom 𝑅 ∪ ran 𝑅)) 

Theorem  relresfld 4790 
Restriction of a relation to its field. (Contributed by FL,
15Apr2012.)

⊢ (Rel 𝑅 → (𝑅 ↾ ∪ ∪ 𝑅)
= 𝑅) 

Theorem  relcoi2 4791 
Composition with the identity relation restricted to a relation's field.
(Contributed by FL, 2May2011.)

⊢ (Rel 𝑅 → (( I ↾ ∪ ∪ 𝑅) ∘ 𝑅) = 𝑅) 

Theorem  relcoi1 4792 
Composition with the identity relation restricted to a relation's field.
(Contributed by FL, 8May2011.)

⊢ (Rel 𝑅 → (𝑅 ∘ ( I ↾ ∪ ∪ 𝑅)) = 𝑅) 

Theorem  unidmrn 4793 
The double union of the converse of a class is its field. (Contributed by
NM, 4Jun2008.)

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

Theorem  relcnvfld 4794 
if 𝑅 is a relation, its double union
equals the double union of its
converse. (Contributed by FL, 5Jan2009.)

⊢ (Rel 𝑅 → ∪ ∪ 𝑅 =
∪ ∪ ^{◡}𝑅) 

Theorem  dfdm2 4795 
Alternate definition of domain dfdm 4298 that doesn't require dummy
variables. (Contributed by NM, 2Aug2010.)

⊢ dom A =
∪ ∪ (^{◡}A
∘ A) 

Theorem  unixpm 4796* 
The double class union of an inhabited cross product is the union of its
members. (Contributed by Jim Kingdon, 18Dec2018.)

⊢ (∃x x ∈ (A ×
B) → ∪
∪ (A ×
B) = (A ∪ B)) 

Theorem  unixp0im 4797 
The union of an empty cross product is empty. (Contributed by Jim
Kingdon, 18Dec2018.)

⊢ ((A ×
B) = ∅ → ∪ (A × B) = ∅) 

Theorem  cnvexg 4798 
The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring]
p. 26. (Contributed by NM, 17Mar1998.)

⊢ (A ∈ 𝑉 → ^{◡}A ∈ V) 

Theorem  cnvex 4799 
The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring]
p. 26. (Contributed by NM, 19Dec2003.)

⊢ A ∈ V ⇒ ⊢ ^{◡}A ∈ V 

Theorem  relcnvexb 4800 
A relation is a set iff its converse is a set. (Contributed by FL,
3Mar2007.)

⊢ (Rel 𝑅 → (𝑅 ∈ V
↔ ^{◡}𝑅 ∈
V)) 