Type  Label  Description 
Statement 

Theorem  dfres2 4601* 
Alternate definition of the restriction operation. (Contributed by
Mario Carneiro, 5Nov2013.)

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

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

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

Theorem  mptresid 4603* 
The restricted identity expressed with the "maps to" notation.
(Contributed by FL, 25Apr2012.)

⊢ (x ∈ A ↦
x) = ( I ↾ A) 

Theorem  dmresi 4604 
The domain of a restricted identity function. (Contributed by NM,
27Aug2004.)

⊢ dom ( I ↾ A) = A 

Theorem  resid 4605 
Any relation restricted to the universe is itself. (Contributed by NM,
16Mar2004.)

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

Theorem  imaeq1 4606 
Equality theorem for image. (Contributed by NM, 14Aug1994.)

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

Theorem  imaeq2 4607 
Equality theorem for image. (Contributed by NM, 14Aug1994.)

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

Theorem  imaeq1i 4608 
Equality theorem for image. (Contributed by NM, 21Dec2008.)

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

Theorem  imaeq2i 4609 
Equality theorem for image. (Contributed by NM, 21Dec2008.)

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

Theorem  imaeq1d 4610 
Equality theorem for image. (Contributed by FL, 15Dec2006.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ → (A “ 𝐶) = (B
“ 𝐶)) 

Theorem  imaeq2d 4611 
Equality theorem for image. (Contributed by FL, 15Dec2006.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ → (𝐶 “ A) = (𝐶 “ B)) 

Theorem  imaeq12d 4612 
Equality theorem for image. (Contributed by Mario Carneiro,
4Dec2016.)

⊢ (φ
→ A = B)
& ⊢ (φ
→ 𝐶 = 𝐷)
⇒ ⊢ (φ → (A “ 𝐶) = (B
“ 𝐷)) 

Theorem  dfima2 4613* 
Alternate definition of image. Compare definition (d) of [Enderton]
p. 44. (Contributed by NM, 19Apr2004.) (Proof shortened by Andrew
Salmon, 27Aug2011.)

⊢ (A “
B) = {y ∣ ∃x ∈ B xAy} 

Theorem  dfima3 4614* 
Alternate definition of image. Compare definition (d) of [Enderton]
p. 44. (Contributed by NM, 14Aug1994.) (Proof shortened by Andrew
Salmon, 27Aug2011.)

⊢ (A “
B) = {y ∣ ∃x(x ∈ B ∧ ⟨x, y⟩
∈ A)} 

Theorem  elimag 4615* 
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 20Jan2007.)

⊢ (A ∈ 𝑉 → (A ∈ (B “ 𝐶) ↔ ∃x ∈ 𝐶 xBA)) 

Theorem  elima 4616* 
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 19Apr2004.)

⊢ A ∈ V ⇒ ⊢ (A ∈ (B “ 𝐶) ↔ ∃x ∈ 𝐶 xBA) 

Theorem  elima2 4617* 
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 11Aug2004.)

⊢ A ∈ V ⇒ ⊢ (A ∈ (B “ 𝐶) ↔ ∃x(x ∈ 𝐶 ∧ xBA)) 

Theorem  elima3 4618* 
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 14Aug1994.)

⊢ A ∈ V ⇒ ⊢ (A ∈ (B “ 𝐶) ↔ ∃x(x ∈ 𝐶 ∧ ⟨x,
A⟩ ∈ B)) 

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

⊢ ℲxA & ⊢
ℲxB ⇒ ⊢ Ⅎx(A “
B) 

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

⊢ (φ
→ ℲxA)
& ⊢ (φ
→ ℲxB) ⇒ ⊢ (φ → Ⅎx(A “
B)) 

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

⊢ (A “
dom A) = ran A 

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

⊢ (A “
B) ⊆ ran A 

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

⊢ (A ∈ 𝑉 → (A “ B)
∈ V) 

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

⊢ ( I “ A) = A 

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

⊢ ran ( I ↾ A) = A 

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

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

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

⊢ (A “
∅) = ∅ 

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

⊢ (∅ “ A) = ∅ 

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

⊢ (A ∈ 𝐶 → ⦋A / x⦌(𝐹 “ B) = (⦋A / x⦌𝐹 “ ⦋A / x⦌B)) 

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

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

Theorem  cnvimarndm 4632 
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  imasng 4633* 
The image of a singleton. (Contributed by NM, 8May2005.)

⊢ (A ∈ B →
(𝑅 “ {A}) = {y
∣ A𝑅y}) 

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

⊢ ((Rel 𝑅 ∧
A ∈
𝑉) → (B ∈ (𝑅 “ {A}) ↔ A𝑅B)) 

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

⊢ B ∈ V
& ⊢ 𝐶 ∈
V ⇒ ⊢ (𝐶 ∈
(A “ {B}) ↔ ⟨B, 𝐶⟩ ∈
A) 

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

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

Theorem  args 4637* 
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.)

⊢ {x ∣
∃y(𝐹 “ {x}) = {y}} =
{x ∣ ∃!y x𝐹y} 

Theorem  eliniseg 4638 
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. (Contributed by
NM, 28Apr2004.) (Proof shortened by Andrew Salmon, 27Aug2011.)

⊢ 𝐶 ∈
V ⇒ ⊢ (B ∈ 𝑉 → (𝐶 ∈ (^{◡}A
“ {B}) ↔ 𝐶AB)) 

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

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

Theorem  iniseg 4640* 
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.)

⊢ (B ∈ 𝑉 → (^{◡}A
“ {B}) = {x ∣ xAB}) 

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

⊢ (𝑅 Se A
↔ ∀x ∈ A (A ∩
(^{◡}𝑅 “ {x})) ∈
V) 

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

⊢ (𝑅 ∈ 𝑉 → 𝑅 Se A) 

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

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

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

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

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

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

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

⊢ Rel ^{◡}A 

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

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

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

⊢ Rel 𝑅 ⇒ ⊢ (A^{◡}𝑅B ↔ B𝑅A) 

Theorem  cotr 4649* 
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.)

⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀x∀y∀z((x𝑅y ∧ y𝑅z) → x𝑅z)) 

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

⊢ (( I ↾ A) ⊆ 𝑅 ↔ ∀x ∈ A x𝑅x) 

Theorem  cnvsym 4651* 
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.)

⊢ (^{◡}𝑅 ⊆ 𝑅 ↔ ∀x∀y(x𝑅y
→ y𝑅x)) 

Theorem  intasym 4652* 
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 ↔ ∀x∀y((x𝑅y ∧ y𝑅x) → x =
y)) 

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

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

Theorem  intirr 4654* 
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 ) = ∅ ↔ ∀x ¬
x𝑅x) 

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

⊢ ((A ∈ 𝑉 ∧
B ∈
𝑊) → (A(^{◡}𝑅 ∘ 𝑅)B
↔ ∃z(A𝑅z ∧ B𝑅z))) 

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

⊢ ((A ×
B) ⊆ (^{◡}𝑅 ∘ 𝑅) ↔ ∀x ∈ A ∀y ∈ B ∃z(x𝑅z ∧ y𝑅z)) 

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

⊢ ((A ×
B) ⊆ (𝑅 ∪ ^{◡}𝑅) ↔ ∀x ∈ A ∀y ∈ B (x𝑅y ∨ y𝑅x)) 

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

⊢ ((A ×
A) ∘ (A × A))
⊆ (A × A) 

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

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

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

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

Theorem  trinxp 4661 
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.)

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

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

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

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

⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((A𝑅B ∧ B𝑅𝐶) → A𝑅𝐶) 

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

⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ¬ (A𝑅B ∧ B𝑅A) 

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

⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((A ∈ 𝑆 ∧ ¬ B𝑅A ∧ B𝑅𝐶) → A𝑅𝐶) 

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

⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐶 ∈ 𝑆 ∧ A𝑅B ∧ ¬ 𝐶𝑅B)
→ A𝑅𝐶) 

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

⊢ (B ∈ 𝑉 → (A(𝑅 ∪ I )B ↔ (A𝑅B ∨ A = B))) 

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

⊢ ((𝑅 Po 𝑋 ∧
(A ∈
𝑋 ∧ B ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((A𝑅B ∧ B(𝑅 ∪ I )𝐶) → A𝑅𝐶)) 

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

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

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

⊢ ^{◡}∅ = ∅ 

Theorem  cnvi 4671 
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 4672 
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.)

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

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

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

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

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

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

⊢ ran (A
∪ B) = (ran A ∪ ran B) 

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

⊢ ran (A
∩ B) ⊆ (ran A ∩ ran B) 

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

⊢ ran ∪
x ∈
A B =
∪ x
∈ A ran
B 

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

⊢ ran ∪ A = ∪ x ∈ A ran x 

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

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

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

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

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

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

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

⊢ ((𝑅 “ A) ∩ B)
⊆ (𝑅 “
(A ∩ (^{◡}𝑅 “ B))) 

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

⊢ ((A ∩
B) “ 𝐶) ⊆ ((A “ 𝐶) ∩ (B “ 𝐶)) 

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

⊢ (𝐶 ∈ 𝑉 → ((A ∩ B)
“ {𝐶}) = ((A “ {𝐶}) ∩ (B “ {𝐶}))) 

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

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

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

⊢ (A ×
∅) = ∅ 

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

⊢ ((∃x x ∈ A ∧ ∃y y ∈ B) ↔
∃z
z ∈
(A × B)) 

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

⊢ ((∃x x ∈ A ∧ ∃y y ∈ B) ↔
∃z
z ∈
(A × B)) 

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

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

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

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

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

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

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

⊢ (B ≠
𝐷 → ((A × {B})
∩ (𝐶 × {𝐷})) = ∅) 

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

⊢ ((A ∩
B) = ∅ → (∪ x ∈ A ({x} × 𝐶) ∩ ∪
y ∈
B ({y}
× 𝐷)) =
∅) 

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

⊢ ((A ∩
B) = ∅ → ((𝐶 ↾ A) ↾ B) =
∅) 

Theorem  rnxpm 4695* 
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.)

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

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

⊢ dom (A
× B) ⊆ A 

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

⊢ ran (A
× B) ⊆ B 

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

⊢ ran (A
× A) = A 

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

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

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

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