Type  Label  Description 
Statement 

Theorem  nfima 4701 
Boundvariable hypothesis builder for image. (Contributed by NM,
30Dec1996.) (Proof shortened by Andrew Salmon, 27Aug2011.)

⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 “ 𝐵) 

Theorem  nfimad 4702 
Deduction version of boundvariable hypothesis builder nfima 4701.
(Contributed by FL, 15Dec2006.) (Revised by Mario Carneiro,
15Oct2016.)

⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝐴 “ 𝐵)) 

Theorem  imadmrn 4703 
The image of the domain of a class is the range of the class.
(Contributed by NM, 14Aug1994.)

⊢ (𝐴 “ dom 𝐴) = ran 𝐴 

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

⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴 

Theorem  imaexg 4705 
The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed
by NM, 24Jul1995.)

⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V) 

Theorem  imai 4706 
Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38.
(Contributed by NM, 30Apr1998.)

⊢ ( I “ 𝐴) = 𝐴 

Theorem  rnresi 4707 
The range of the restricted identity function. (Contributed by NM,
27Aug2004.)

⊢ ran ( I ↾ 𝐴) = 𝐴 

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

⊢ (𝐵 ⊆ 𝐴 → (( I ↾ 𝐴) “ 𝐵) = 𝐵) 

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

⊢ (𝐴 “ ∅) =
∅ 

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

⊢ (∅ “ 𝐴) = ∅ 

Theorem  csbima12g 4711 
Move class substitution in and out of the image of a function.
(Contributed by FL, 15Dec2006.) (Proof shortened by Mario Carneiro,
4Dec2016.)

⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵)) 

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

⊢ ((𝐴 “ 𝐵) = ∅ ↔ (dom 𝐴 ∩ 𝐵) = ∅) 

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

⊢ (^{◡}𝐴 “ 𝐵) ⊆ dom 𝐴 

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

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

Theorem  imasng 4715* 
The image of a singleton. (Contributed by NM, 8May2005.)

⊢ (𝐴 ∈ 𝐵 → (𝑅 “ {𝐴}) = {𝑦 ∣ 𝐴𝑅𝑦}) 

Theorem  elreimasng 4716 
Elementhood in the image of a singleton. (Contributed by Jim Kingdon,
10Dec2018.)

⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑉) → (𝐵 ∈ (𝑅 “ {𝐴}) ↔ 𝐴𝑅𝐵)) 

Theorem  elimasn 4717 
Membership in an image of a singleton. (Contributed by NM,
15Mar2004.) (Proof shortened by Andrew Salmon, 27Aug2011.)

⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈
V ⇒ ⊢ (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴) 

Theorem  elimasng 4718 
Membership in an image of a singleton. (Contributed by Raph Levien,
21Oct2006.)

⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)) 

Theorem  args 4719* 
Two ways to express the class of uniquevalued arguments of 𝐹,
which is the same as the domain of 𝐹 whenever 𝐹 is a function.
The lefthand side of the equality is from Definition 10.2 of [Quine]
p. 65. Quine uses the notation "arg 𝐹 " for this class
(for which
we have no separate notation). (Contributed by NM, 8May2005.)

⊢ {𝑥 ∣ ∃𝑦(𝐹 “ {𝑥}) = {𝑦}} = {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦} 

Theorem  eliniseg 4720 
Membership in an initial segment. The idiom (^{◡}𝐴 “ {𝐵}),
meaning {𝑥 ∣ 𝑥𝐴𝐵}, is used to specify an initial
segment in
(for example) Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by
NM, 28Apr2004.) (Proof shortened by Andrew Salmon, 27Aug2011.)

⊢ 𝐶 ∈ V ⇒ ⊢ (𝐵 ∈ 𝑉 → (𝐶 ∈ (^{◡}𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵)) 

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

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

Theorem  iniseg 4722* 
An idiom that signifies an initial segment of an ordering, used, for
example, in Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by
NM, 28Apr2004.)

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

Theorem  dfse2 4723* 
Alternate definition of setlike relation. (Contributed by Mario
Carneiro, 23Jun2015.)

⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 (𝐴 ∩ (^{◡}𝑅 “ {𝑥})) ∈ V) 

Theorem  exse2 4724 
Any set relation is setlike. (Contributed by Mario Carneiro,
22Jun2015.)

⊢ (𝑅 ∈ 𝑉 → 𝑅 Se 𝐴) 

Theorem  imass1 4725 
Subset theorem for image. (Contributed by NM, 16Mar2004.)

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

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

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

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

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

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

⊢ Rel ^{◡}𝐴 

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

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

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

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

Theorem  cotr 4731* 
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 4732* 
Two ways to state a relation is reflexive. Adapted from Tarski.
(Contributed by FL, 15Jan2012.) (Revised by NM, 30Mar2016.)

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

Theorem  cnvsym 4733* 
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 4734* 
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 4735* 
Two ways of saying a relation is antisymmetric and reflexive.
∪ ∪ 𝑅 is the field of a relation by relfld 4871. (Contributed by
NM, 6May2008.) (Proof shortened by Andrew Salmon, 27Aug2011.)

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

Theorem  intirr 4736* 
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 4737* 
Two ways of saying that two elements have an upper bound. (Contributed
by Mario Carneiro, 3Nov2015.)

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

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

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

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

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

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

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

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

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

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

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

Theorem  trinxp 4743 
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 4744 
A strict order relation is irreflexive. (Contributed by NM,
10Feb1996.) (Revised by Mario Carneiro, 10May2013.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ ^{◡}∅ = ∅ 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ dom (𝐴 × 𝐵) ⊆ 𝐴 

Theorem  rnxpss 4779 
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 4780 
The range of a square cross product. (Contributed by FL,
17May2010.)

⊢ ran (𝐴 × 𝐴) = 𝐴 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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