Type  Label  Description 
Statement 

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

⊢ ^{◡}∅ = ∅ 

Theorem  cnvi 4802 
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 4803 
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 4804 
Distributive law for converse over set difference. (Contributed by
Mario Carneiro, 26Jun2014.)

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

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

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

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

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

Theorem  rnin 4807 
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 4808 
The range of an indexed union. (Contributed by Mario Carneiro,
29May2015.)

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

Theorem  rnuni 4809* 
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 4810 
Distributive law for image over union. Theorem 35 of [Suppes] p. 65.
(Contributed by NM, 30Sep2002.)

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

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

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

Theorem  dminss 4812 
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 4813 
An upper bound for intersection with an image. Theorem 41 of [Suppes]
p. 66. (Contributed by NM, 11Aug2004.)

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

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

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

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

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

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

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

Theorem  xp0 4817 
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 4818* 
The cross product of inhabited classes is inhabited. (Contributed by
Jim Kingdon, 11Dec2018.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem  rnxpm 4826* 
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 4827 
The domain of a cross product is a subclass of the first factor.
(Contributed by NM, 19Mar2007.)

⊢ dom (𝐴 × 𝐵) ⊆ 𝐴 

Theorem  rnxpss 4828 
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  dmxpss2 4829 
Upper bound for the domain of a binary relation. (Contributed by BJ,
10Jul2022.)

⊢ (𝑅 ⊆ (𝐴 × 𝐵) → dom 𝑅 ⊆ 𝐴) 

Theorem  rnxpss2 4830 
Upper bound for the range of a binary relation. (Contributed by BJ,
10Jul2022.)

⊢ (𝑅 ⊆ (𝐴 × 𝐵) → ran 𝑅 ⊆ 𝐵) 

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

⊢ ran (𝐴 × 𝐴) = 𝐴 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ dom (𝐴 ↾ V) = dom 𝐴 

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

⊢ ran (𝐴 ↾ V) = ran 𝐴 

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

⊢ ran 𝐴 = (𝐴 “ V) 

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

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

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

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

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

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

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

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

Theorem  dmsnm 4862* 
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 4863* 
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 4864 
The domain of the singleton of the empty set is empty. (Contributed by
NM, 30Jan2004.)

⊢ dom {∅} = ∅ 

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

⊢ ^{◡}{∅} = ∅ 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem  rnsnopg 4875 
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 4876 
The range of a pair of ordered pairs is the pair of second members.
(Contributed by Thierry Arnoux, 3Jan2017.)

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

Theorem  rnsnop 4877 
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.)

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

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

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

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

⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ^{◡}{⟨𝐴, 𝐵⟩} = {⟨𝐵, 𝐴⟩} 

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

⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∩
∩ ∩ ^{◡}{⟨𝐴, 𝐵⟩} = 𝐵 

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

⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∪
ran {⟨𝐴, 𝐵⟩} = 𝐵 

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

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

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

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

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

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

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

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

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

⊢ (^{◡}(𝐹 ↾ 𝐴) “ 𝐵) = ((^{◡}𝐹 “ 𝐵) ∩ 𝐴) 

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

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

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

⊢ (𝐴 ↾ dom (𝐴 ↾ 𝐵)) = (𝐴 ↾ 𝐵) 

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

⊢ (𝐴 “ dom (𝐴 ↾ 𝐵)) = (𝐴 “ 𝐵) 

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

⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (^{◡}𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶} 

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

⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝐶 ∈ 𝑉 → (^{◡}𝐹 “ {𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐵 = 𝐶}) 

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

⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} 

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

⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 

Theorem  dmmptg 4894* 
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.)

⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) 

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

⊢ Rel (𝐴 ∘ 𝐵) 

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

⊢ (𝐴 ∘ 𝐵) = ∪
𝑥 ∈ V ((^{◡}𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) 

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

⊢ ((dom 𝐴 ∩ ran 𝐵) ⊆ 𝐶 → (𝐴 ∘ 𝐵) = ∪
𝑥 ∈ 𝐶 ((^{◡}𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))) 

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

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

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

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

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

⊢ (ran 𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ∘ 𝐵) = (𝐴 ∘ 𝐵)) 