Type  Label  Description 
Statement 

Theorem  iss 4801 
A subclass of the identity function is the identity function restricted
to its domain. (Contributed by NM, 13Dec2003.) (Proof shortened by
Andrew Salmon, 27Aug2011.)

⊢ (𝐴 ⊆ I ↔ 𝐴 = ( I ↾ dom 𝐴)) 

Theorem  resopab2 4802* 
Restriction of a class abstraction of ordered pairs. (Contributed by
NM, 24Aug2007.)

⊢ (𝐴 ⊆ 𝐵 → ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}) 

Theorem  resmpt 4803* 
Restriction of the mapping operation. (Contributed by Mario Carneiro,
15Jul2013.)

⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶)) 

Theorem  resmpt3 4804* 
Unconditional restriction of the mapping operation. (Contributed by
Stefan O'Rear, 24Jan2015.) (Proof shortened by Mario Carneiro,
22Mar2015.)

⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ (𝐴 ∩ 𝐵) ↦ 𝐶) 

Theorem  resmptf 4805 
Restriction of the mapping operation. (Contributed by Thierry Arnoux,
28Mar2017.)

⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶)) 

Theorem  resmptd 4806* 
Restriction of the mapping operation, deduction form. (Contributed by
Glauco Siliprandi, 11Dec2019.)

⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶)) 

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

⊢ (𝑅 ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥𝑅𝑦)} 

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

⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)} = ( I ↾ 𝐴) 

Theorem  mptresid 4809* 
The restricted identity expressed with the mapsto notation.
(Contributed by FL, 25Apr2012.)

⊢ (𝑥 ∈ 𝐴 ↦ 𝑥) = ( I ↾ 𝐴) 

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

⊢ dom ( I ↾ 𝐴) = 𝐴 

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

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

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

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

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

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

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

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

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

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

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

⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶)) 

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

⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵)) 

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

⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐷)) 

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

⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑥𝐴𝑦} 

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

⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} 

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

⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥 ∈ 𝐶 𝑥𝐵𝐴)) 

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

⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥 ∈ 𝐶 𝑥𝐵𝐴) 

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

⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ 𝑥𝐵𝐴)) 

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

⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ ⟨𝑥, 𝐴⟩ ∈ 𝐵)) 

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

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

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

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

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

⊢ (𝐴 “ dom 𝐴) = ran 𝐴 

Theorem  imassrn 4828 
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 4829 
The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed
by NM, 24Jul1995.)

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

Theorem  imaex 4830 
The image of a set is a set. Theorem 3.17 of [Monk1] p. 39.
(Contributed by JJ, 24Sep2021.)

⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 “ 𝐵) ∈ V 

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

⊢ ( I “ 𝐴) = 𝐴 

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

⊢ ran ( I ↾ 𝐴) = 𝐴 

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

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

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

⊢ (𝐴 “ ∅) =
∅ 

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

⊢ (∅ “ 𝐴) = ∅ 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem  args 4844* 
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 4845 
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 4846 
Any set is equal to its preimage under the converse epsilon relation.
(Contributed by Mario Carneiro, 9Mar2013.)

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

Theorem  iniseg 4847* 
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 4848* 
Alternate definition of setlike relation. (Contributed by Mario
Carneiro, 23Jun2015.)

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

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

⊢ (𝑅 ∈ 𝑉 → 𝑅 Se 𝐴) 

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

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

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

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

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

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

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

⊢ Rel ^{◡}𝐴 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem  mptcnv 4877* 
The converse of a mapping function. (Contributed by Thierry Arnoux,
16Jan2017.)

⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → ^{◡}(𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐶 ↦ 𝐷)) 

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

⊢ ^{◡}∅ = ∅ 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem  sqxpeq0 4898 
A Cartesian square is empty iff its member is empty. (Contributed by Jim
Kingdon, 21Apr2023.)

⊢ ((𝐴 × 𝐴) = ∅ ↔ 𝐴 = ∅) 

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

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

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

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