Type  Label  Description 
Statement 

Definition  dfima 4301 
Define the image of a class (as restricted by another class).
Definition 6.6(2) of [TakeutiZaring] p. 24. For example, ( F = {
⟨
2 , 6 ⟩, ⟨ 3 ,
9 ⟩ } /\ B = { 1 , 2 } ) > ( F “ B )
= { 6 } . Contrast with restriction (dfres 4300) and range
(dfrn 4299). For an alternate definition, see dfima2 4613. (Contributed
by NM, 2Aug1994.)

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

Theorem  xpeq1 4302 
Equality theorem for cross product. (Contributed by NM, 4Jul1994.)

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

Theorem  xpeq2 4303 
Equality theorem for cross product. (Contributed by NM, 5Jul1994.)

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

Theorem  elxpi 4304* 
Membership in a cross product. Uses fewer axioms than elxp 4305.
(Contributed by NM, 4Jul1994.)

⊢ (A ∈ (B ×
𝐶) → ∃x∃y(A = ⟨x,
y⟩ ∧
(x ∈
B ∧
y ∈
𝐶))) 

Theorem  elxp 4305* 
Membership in a cross product. (Contributed by NM, 4Jul1994.)

⊢ (A ∈ (B ×
𝐶) ↔ ∃x∃y(A = ⟨x,
y⟩ ∧
(x ∈
B ∧
y ∈
𝐶))) 

Theorem  elxp2 4306* 
Membership in a cross product. (Contributed by NM, 23Feb2004.)

⊢ (A ∈ (B ×
𝐶) ↔ ∃x ∈ B ∃y ∈ 𝐶 A =
⟨x, y⟩) 

Theorem  xpeq12 4307 
Equality theorem for cross product. (Contributed by FL, 31Aug2009.)

⊢ ((A =
B ∧ 𝐶 = 𝐷) → (A × 𝐶) = (B
× 𝐷)) 

Theorem  xpeq1i 4308 
Equality inference for cross product. (Contributed by NM,
21Dec2008.)

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

Theorem  xpeq2i 4309 
Equality inference for cross product. (Contributed by NM,
21Dec2008.)

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

Theorem  xpeq12i 4310 
Equality inference for cross product. (Contributed by FL,
31Aug2009.)

⊢ A =
B & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (A × 𝐶) = (B
× 𝐷) 

Theorem  xpeq1d 4311 
Equality deduction for cross product. (Contributed by Jeff Madsen,
17Jun2010.)

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

Theorem  xpeq2d 4312 
Equality deduction for cross product. (Contributed by Jeff Madsen,
17Jun2010.)

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

Theorem  xpeq12d 4313 
Equality deduction for cross product. (Contributed by NM,
8Dec2013.)

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

Theorem  nfxp 4314 
Boundvariable hypothesis builder for cross product. (Contributed by
NM, 15Sep2003.) (Revised by Mario Carneiro, 15Oct2016.)

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

Theorem  0nelxp 4315 
The empty set is not a member of a cross product. (Contributed by NM,
2May1996.) (Revised by Mario Carneiro, 26Apr2015.)

⊢ ¬ ∅ ∈ (A ×
B) 

Theorem  0nelelxp 4316 
A member of a cross product (ordered pair) doesn't contain the empty
set. (Contributed by NM, 15Dec2008.)

⊢ (𝐶 ∈
(A × B) → ¬ ∅ ∈ 𝐶) 

Theorem  opelxp 4317 
Ordered pair membership in a cross product. (Contributed by NM,
15Nov1994.) (Proof shortened by Andrew Salmon, 12Aug2011.)
(Revised by Mario Carneiro, 26Apr2015.)

⊢ (⟨A,
B⟩ ∈ (𝐶 × 𝐷) ↔ (A ∈ 𝐶 ∧ B ∈ 𝐷)) 

Theorem  brxp 4318 
Binary relation on a cross product. (Contributed by NM,
22Apr2004.)

⊢ (A(𝐶 × 𝐷)B
↔ (A ∈ 𝐶 ∧
B ∈
𝐷)) 

Theorem  opelxpi 4319 
Ordered pair membership in a cross product (implication). (Contributed by
NM, 28May1995.)

⊢ ((A ∈ 𝐶 ∧
B ∈
𝐷) → ⟨A, B⟩
∈ (𝐶 × 𝐷)) 

Theorem  opelxp1 4320 
The first member of an ordered pair of classes in a cross product belongs
to first cross product argument. (Contributed by NM, 28May2008.)
(Revised by Mario Carneiro, 26Apr2015.)

⊢ (⟨A,
B⟩ ∈ (𝐶 × 𝐷) → A ∈ 𝐶) 

Theorem  opelxp2 4321 
The second member of an ordered pair of classes in a cross product belongs
to second cross product argument. (Contributed by Mario Carneiro,
26Apr2015.)

⊢ (⟨A,
B⟩ ∈ (𝐶 × 𝐷) → B ∈ 𝐷) 

Theorem  otelxp1 4322 
The first member of an ordered triple of classes in a cross product
belongs to first cross product argument. (Contributed by NM,
28May2008.)

⊢ (⟨⟨A, B⟩,
𝐶⟩ ∈ ((𝑅 × 𝑆) × 𝑇) → A ∈ 𝑅) 

Theorem  rabxp 4323* 
Membership in a class builder restricted to a cross product.
(Contributed by NM, 20Feb2014.)

⊢ (x =
⟨y, z⟩ → (φ ↔ ψ)) ⇒ ⊢ {x ∈ (A × B)
∣ φ} = {⟨y, z⟩
∣ (y ∈ A ∧ z ∈ B ∧ ψ)} 

Theorem  brrelex12 4324 
A true binary relation on a relation implies the arguments are sets.
(This is a property of our ordered pair definition.) (Contributed by
Mario Carneiro, 26Apr2015.)

⊢ ((Rel 𝑅 ∧
A𝑅B)
→ (A ∈ V ∧ B ∈
V)) 

Theorem  brrelex 4325 
A true binary relation on a relation implies the first argument is a set.
(This is a property of our ordered pair definition.) (Contributed by NM,
18May2004.) (Revised by Mario Carneiro, 26Apr2015.)

⊢ ((Rel 𝑅 ∧
A𝑅B)
→ A ∈ V) 

Theorem  brrelex2 4326 
A true binary relation on a relation implies the second argument is a
set. (This is a property of our ordered pair definition.) (Contributed
by Mario Carneiro, 26Apr2015.)

⊢ ((Rel 𝑅 ∧
A𝑅B)
→ B ∈ V) 

Theorem  brrelexi 4327 
The first argument of a binary relation exists. (An artifact of our
ordered pair definition.) (Contributed by NM, 4Jun1998.)

⊢ Rel 𝑅 ⇒ ⊢ (A𝑅B
→ A ∈ V) 

Theorem  brrelex2i 4328 
The second argument of a binary relation exists. (An artifact of our
ordered pair definition.) (Contributed by Mario Carneiro,
26Apr2015.)

⊢ Rel 𝑅 ⇒ ⊢ (A𝑅B
→ B ∈ V) 

Theorem  nprrel 4329 
No proper class is related to anything via any relation. (Contributed
by Roy F. Longton, 30Jul2005.)

⊢ Rel 𝑅
& ⊢ ¬ A
∈ V ⇒ ⊢ ¬ A𝑅B 

Theorem  fconstmpt 4330* 
Representation of a constant function using the mapping operation.
(Note that x
cannot appear free in B.) (Contributed by NM,
12Oct1999.) (Revised by Mario Carneiro, 16Nov2013.)

⊢ (A ×
{B}) = (x ∈ A ↦ B) 

Theorem  vtoclr 4331* 
Variable to class conversion of transitive relation. (Contributed by
NM, 9Jun1998.) (Revised by Mario Carneiro, 26Apr2015.)

⊢ Rel 𝑅
& ⊢ ((x𝑅y ∧ y𝑅z)
→ x𝑅z) ⇒ ⊢ ((A𝑅B ∧ B𝑅𝐶) → A𝑅𝐶) 

Theorem  opelvvg 4332 
Ordered pair membership in the universal class of ordered pairs.
(Contributed by Mario Carneiro, 3May2015.)

⊢ ((A ∈ 𝑉 ∧
B ∈
𝑊) → ⟨A, B⟩
∈ (V × V)) 

Theorem  opelvv 4333 
Ordered pair membership in the universal class of ordered pairs.
(Contributed by NM, 22Aug2013.) (Revised by Mario Carneiro,
26Apr2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ⟨A, B⟩
∈ (V × V) 

Theorem  opthprc 4334 
Justification theorem for an ordered pair definition that works for any
classes, including proper classes. This is a possible definition
implied by the footnote in [Jech] p. 78,
which says, "The sophisticated
reader will not object to our use of a pair of classes."
(Contributed
by NM, 28Sep2003.)

⊢ (((A
× {∅}) ∪ (B ×
{{∅}})) = ((𝐶
× {∅}) ∪ (𝐷 × {{∅}})) ↔ (A = 𝐶 ∧
B = 𝐷)) 

Theorem  brel 4335 
Two things in a binary relation belong to the relation's domain.
(Contributed by NM, 17May1996.) (Revised by Mario Carneiro,
26Apr2015.)

⊢ 𝑅 ⊆ (𝐶 × 𝐷) ⇒ ⊢ (A𝑅B
→ (A ∈ 𝐶 ∧
B ∈
𝐷)) 

Theorem  brab2a 4336* 
Ordered pair membership in an ordered pair class abstraction.
(Contributed by Mario Carneiro, 9Nov2015.)

⊢ ((x =
A ∧
y = B)
→ (φ ↔ ψ)) & ⊢ 𝑅 = {⟨x, y⟩
∣ ((x ∈ 𝐶 ∧
y ∈
𝐷) ∧ φ)} ⇒ ⊢ (A𝑅B
↔ ((A ∈ 𝐶 ∧
B ∈
𝐷) ∧ ψ)) 

Theorem  elxp3 4337* 
Membership in a cross product. (Contributed by NM, 5Mar1995.)

⊢ (A ∈ (B ×
𝐶) ↔ ∃x∃y(⟨x,
y⟩ = A ∧ ⟨x, y⟩
∈ (B
× 𝐶))) 

Theorem  opeliunxp 4338 
Membership in a union of cross products. (Contributed by Mario
Carneiro, 29Dec2014.) (Revised by Mario Carneiro, 1Jan2017.)

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

Theorem  xpundi 4339 
Distributive law for cross product over union. Theorem 103 of [Suppes]
p. 52. (Contributed by NM, 12Aug2004.)

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

Theorem  xpundir 4340 
Distributive law for cross product over union. Similar to Theorem 103
of [Suppes] p. 52. (Contributed by NM,
30Sep2002.)

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

Theorem  xpiundi 4341* 
Distributive law for cross product over indexed union. (Contributed by
Mario Carneiro, 27Apr2014.)

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

Theorem  xpiundir 4342* 
Distributive law for cross product over indexed union. (Contributed by
Mario Carneiro, 27Apr2014.)

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

Theorem  iunxpconst 4343* 
Membership in a union of cross products when the second factor is
constant. (Contributed by Mario Carneiro, 29Dec2014.)

⊢ ∪ x ∈ A ({x} ×
B) = (A × B) 

Theorem  xpun 4344 
The cross product of two unions. (Contributed by NM, 12Aug2004.)

⊢ ((A ∪
B) × (𝐶 ∪ 𝐷)) = (((A × 𝐶) ∪ (A × 𝐷)) ∪ ((B × 𝐶) ∪ (B × 𝐷))) 

Theorem  elvv 4345* 
Membership in universal class of ordered pairs. (Contributed by NM,
4Jul1994.)

⊢ (A ∈ (V × V) ↔ ∃x∃y A = ⟨x,
y⟩) 

Theorem  elvvv 4346* 
Membership in universal class of ordered triples. (Contributed by NM,
17Dec2008.)

⊢ (A ∈ ((V × V) × V) ↔ ∃x∃y∃z A = ⟨⟨x, y⟩,
z⟩) 

Theorem  elvvuni 4347 
An ordered pair contains its union. (Contributed by NM,
16Sep2006.)

⊢ (A ∈ (V × V) → ∪ A ∈ A) 

Theorem  mosubopt 4348* 
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28Aug2007.)

⊢ (∀y∀z∃*xφ →
∃*x∃y∃z(A =
⟨y, z⟩ ∧ φ)) 

Theorem  mosubop 4349* 
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28May1995.)

⊢ ∃*xφ ⇒ ⊢ ∃*x∃y∃z(A = ⟨y,
z⟩ ∧
φ) 

Theorem  brinxp2 4350 
Intersection of binary relation with cross product. (Contributed by NM,
3Mar2007.) (Revised by Mario Carneiro, 26Apr2015.)

⊢ (A(𝑅 ∩ (𝐶 × 𝐷))B
↔ (A ∈ 𝐶 ∧
B ∈
𝐷 ∧ A𝑅B)) 

Theorem  brinxp 4351 
Intersection of binary relation with cross product. (Contributed by NM,
9Mar1997.)

⊢ ((A ∈ 𝐶 ∧
B ∈
𝐷) → (A𝑅B
↔ A(𝑅 ∩ (𝐶 × 𝐷))B)) 

Theorem  poinxp 4352 
Intersection of partial order with cross product of its field.
(Contributed by Mario Carneiro, 10Jul2014.)

⊢ (𝑅 Po A
↔ (𝑅 ∩ (A × A))
Po A) 

Theorem  soinxp 4353 
Intersection of linear order with cross product of its field.
(Contributed by Mario Carneiro, 10Jul2014.)

⊢ (𝑅 Or A
↔ (𝑅 ∩ (A × A))
Or A) 

Theorem  seinxp 4354 
Intersection of setlike relation with cross product of its field.
(Contributed by Mario Carneiro, 22Jun2015.)

⊢ (𝑅 Se A
↔ (𝑅 ∩ (A × A))
Se A) 

Theorem  posng 4355 
Partial ordering of a singleton. (Contributed by Jim Kingdon,
5Dec2018.)

⊢ ((Rel 𝑅 ∧
A ∈ V)
→ (𝑅 Po {A} ↔ ¬ A𝑅A)) 

Theorem  sosng 4356 
Strict linear ordering on a singleton. (Contributed by Jim Kingdon,
5Dec2018.)

⊢ ((Rel 𝑅 ∧
A ∈ V)
→ (𝑅 Or {A} ↔ ¬ A𝑅A)) 

Theorem  opabssxp 4357* 
An abstraction relation is a subset of a related cross product.
(Contributed by NM, 16Jul1995.)

⊢ {⟨x,
y⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} ⊆ (A × B) 

Theorem  brab2ga 4358* 
The law of concretion for a binary relation. See brab2a 4336 for alternate
proof. TODO: should one of them be deleted? (Contributed by Mario
Carneiro, 28Apr2015.) (Proof modification is discouraged.)

⊢ ((x =
A ∧
y = B)
→ (φ ↔ ψ)) & ⊢ 𝑅 = {⟨x, y⟩
∣ ((x ∈ 𝐶 ∧
y ∈
𝐷) ∧ φ)} ⇒ ⊢ (A𝑅B
↔ ((A ∈ 𝐶 ∧
B ∈
𝐷) ∧ ψ)) 

Theorem  optocl 4359* 
Implicit substitution of class for ordered pair. (Contributed by NM,
5Mar1995.)

⊢ 𝐷 = (B
× 𝐶) & ⊢
(⟨x, y⟩ = A
→ (φ ↔ ψ)) & ⊢ ((x ∈ B ∧ y ∈ 𝐶) → φ) ⇒ ⊢ (A ∈ 𝐷 → ψ) 

Theorem  2optocl 4360* 
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12Mar1995.)

⊢ 𝑅 = (𝐶 × 𝐷)
& ⊢ (⟨x,
y⟩ = A → (φ
↔ ψ)) & ⊢
(⟨z, w⟩ = B
→ (ψ ↔ χ)) & ⊢ (((x ∈ 𝐶 ∧ y ∈ 𝐷) ∧
(z ∈
𝐶 ∧ w ∈ 𝐷)) → φ) ⇒ ⊢ ((A ∈ 𝑅 ∧ B ∈ 𝑅) → χ) 

Theorem  3optocl 4361* 
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12Mar1995.)

⊢ 𝑅 = (𝐷 × 𝐹)
& ⊢ (⟨x,
y⟩ = A → (φ
↔ ψ)) & ⊢
(⟨z, w⟩ = B
→ (ψ ↔ χ)) & ⊢
(⟨v, u⟩ = 𝐶 → (χ ↔ θ)) & ⊢ (((x ∈ 𝐷 ∧ y ∈ 𝐹) ∧
(z ∈
𝐷 ∧ w ∈ 𝐹) ∧
(v ∈
𝐷 ∧ u ∈ 𝐹)) → φ) ⇒ ⊢ ((A ∈ 𝑅 ∧ B ∈ 𝑅 ∧ 𝐶 ∈ 𝑅) → θ) 

Theorem  opbrop 4362* 
Ordered pair membership in a relation. Special case. (Contributed by
NM, 5Aug1995.)

⊢ (((z =
A ∧
w = B)
∧ (v =
𝐶 ∧ u = 𝐷)) → (φ ↔ ψ)) & ⊢ 𝑅 = {⟨x, y⟩
∣ ((x ∈ (𝑆 × 𝑆) ∧
y ∈
(𝑆 × 𝑆)) ∧ ∃z∃w∃v∃u((x =
⟨z, w⟩ ∧ y = ⟨v,
u⟩) ∧ φ))} ⇒ ⊢ (((A ∈ 𝑆 ∧ B ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (⟨A, B⟩𝑅⟨𝐶, 𝐷⟩ ↔ ψ)) 

Theorem  0xp 4363 
The cross product with the empty set is empty. Part of Theorem 3.13(ii)
of [Monk1] p. 37. (Contributed by NM,
4Jul1994.)

⊢ (∅ × A) = ∅ 

Theorem  csbxpg 4364 
Distribute proper substitution through the cross product of two
classes. (Contributed by Alan Sare, 10Nov2012.)

⊢ (A ∈ 𝐷 → ⦋A / x⦌(B × 𝐶) = (⦋A / x⦌B × ⦋A / x⦌𝐶)) 

Theorem  releq 4365 
Equality theorem for the relation predicate. (Contributed by NM,
1Aug1994.)

⊢ (A =
B → (Rel A ↔ Rel B)) 

Theorem  releqi 4366 
Equality inference for the relation predicate. (Contributed by NM,
8Dec2006.)

⊢ A =
B ⇒ ⊢ (Rel A ↔ Rel B) 

Theorem  releqd 4367 
Equality deduction for the relation predicate. (Contributed by NM,
8Mar2014.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ → (Rel A ↔ Rel B)) 

Theorem  nfrel 4368 
Boundvariable hypothesis builder for a relation. (Contributed by NM,
31Jan2004.) (Revised by Mario Carneiro, 15Oct2016.)

⊢ ℲxA ⇒ ⊢ ℲxRel A 

Theorem  sbcrel 4369 
Distribute proper substitution through a relation predicate. (Contributed
by Alexander van der Vekens, 23Jul2017.)

⊢ (A ∈ 𝑉 → ([A / x]Rel 𝑅 ↔ Rel ⦋A / x⦌𝑅)) 

Theorem  relss 4370 
Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58.
(Contributed by NM, 15Aug1994.)

⊢ (A ⊆
B → (Rel B → Rel A)) 

Theorem  ssrel 4371* 
A subclass relationship depends only on a relation's ordered pairs.
Theorem 3.2(i) of [Monk1] p. 33.
(Contributed by NM, 2Aug1994.)
(Proof shortened by Andrew Salmon, 27Aug2011.)

⊢ (Rel A
→ (A ⊆ B ↔ ∀x∀y(⟨x,
y⟩ ∈ A →
⟨x, y⟩ ∈
B))) 

Theorem  eqrel 4372* 
Extensionality principle for relations. Theorem 3.2(ii) of [Monk1]
p. 33. (Contributed by NM, 2Aug1994.)

⊢ ((Rel A
∧ Rel B)
→ (A = B ↔ ∀x∀y(⟨x,
y⟩ ∈ A ↔
⟨x, y⟩ ∈
B))) 

Theorem  ssrel2 4373* 
A subclass relationship depends only on a relation's ordered pairs.
This version of ssrel 4371 is restricted to the relation's domain.
(Contributed by Thierry Arnoux, 25Jan2018.)

⊢ (𝑅 ⊆ (A × B)
→ (𝑅 ⊆ 𝑆 ↔ ∀x ∈ A ∀y ∈ B
(⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩
∈ 𝑆))) 

Theorem  relssi 4374* 
Inference from subclass principle for relations. (Contributed by NM,
31Mar1998.)

⊢ Rel A
& ⊢ (⟨x,
y⟩ ∈ A →
⟨x, y⟩ ∈
B) ⇒ ⊢ A ⊆ B 

Theorem  relssdv 4375* 
Deduction from subclass principle for relations. (Contributed by NM,
11Sep2004.)

⊢ (φ
→ Rel A) & ⊢ (φ → (⟨x, y⟩
∈ A
→ ⟨x, y⟩ ∈
B)) ⇒ ⊢ (φ → A ⊆ B) 

Theorem  eqrelriv 4376* 
Inference from extensionality principle for relations. (Contributed by
FL, 15Oct2012.)

⊢ (⟨x,
y⟩ ∈ A ↔
⟨x, y⟩ ∈
B) ⇒ ⊢ ((Rel A ∧ Rel B) → A =
B) 

Theorem  eqrelriiv 4377* 
Inference from extensionality principle for relations. (Contributed by
NM, 17Mar1995.)

⊢ Rel A
& ⊢ Rel B
& ⊢ (⟨x,
y⟩ ∈ A ↔
⟨x, y⟩ ∈
B) ⇒ ⊢ A = B 

Theorem  eqbrriv 4378* 
Inference from extensionality principle for relations. (Contributed by
NM, 12Dec2006.)

⊢ Rel A
& ⊢ Rel B
& ⊢ (xAy ↔
xBy) ⇒ ⊢ A = B 

Theorem  eqrelrdv 4379* 
Deduce equality of relations from equivalence of membership.
(Contributed by Rodolfo Medina, 10Oct2010.)

⊢ Rel A
& ⊢ Rel B
& ⊢ (φ
→ (⟨x, y⟩ ∈
A ↔ ⟨x, y⟩
∈ B)) ⇒ ⊢ (φ → A = B) 

Theorem  eqbrrdv 4380* 
Deduction from extensionality principle for relations. (Contributed by
Mario Carneiro, 3Jan2017.)

⊢ (φ
→ Rel A) & ⊢ (φ → Rel B)
& ⊢ (φ
→ (xAy ↔
xBy)) ⇒ ⊢ (φ → A = B) 

Theorem  eqbrrdiv 4381* 
Deduction from extensionality principle for relations. (Contributed by
Rodolfo Medina, 10Oct2010.)

⊢ Rel A
& ⊢ Rel B
& ⊢ (φ
→ (xAy ↔
xBy)) ⇒ ⊢ (φ → A = B) 

Theorem  eqrelrdv2 4382* 
A version of eqrelrdv 4379. (Contributed by Rodolfo Medina,
10Oct2010.)

⊢ (φ
→ (⟨x, y⟩ ∈
A ↔ ⟨x, y⟩
∈ B)) ⇒ ⊢ (((Rel A ∧ Rel B) ∧ φ) → A = B) 

Theorem  ssrelrel 4383* 
A subclass relationship determined by ordered triples. Use relrelss 4787
to express the antecedent in terms of the relation predicate.
(Contributed by NM, 17Dec2008.) (Proof shortened by Andrew Salmon,
27Aug2011.)

⊢ (A ⊆
((V × V) × V) → (A
⊆ B ↔ ∀x∀y∀z(⟨⟨x, y⟩,
z⟩ ∈ A →
⟨⟨x, y⟩, z⟩ ∈
B))) 

Theorem  eqrelrel 4384* 
Extensionality principle for ordered triples, analogous to eqrel 4372.
Use relrelss 4787 to express the antecedent in terms of the
relation
predicate. (Contributed by NM, 17Dec2008.)

⊢ ((A ∪
B) ⊆ ((V × V) × V)
→ (A = B ↔ ∀x∀y∀z(⟨⟨x, y⟩,
z⟩ ∈ A ↔
⟨⟨x, y⟩, z⟩ ∈
B))) 

Theorem  elrel 4385* 
A member of a relation is an ordered pair. (Contributed by NM,
17Sep2006.)

⊢ ((Rel 𝑅 ∧
A ∈
𝑅) → ∃x∃y A = ⟨x,
y⟩) 

Theorem  relsn 4386 
A singleton is a relation iff it is an ordered pair. (Contributed by
NM, 24Sep2013.)

⊢ A ∈ V ⇒ ⊢ (Rel {A} ↔ A
∈ (V × V)) 

Theorem  relsnop 4387 
A singleton of an ordered pair is a relation. (Contributed by NM,
17May1998.) (Revised by Mario Carneiro, 26Apr2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ Rel {⟨A, B⟩} 

Theorem  xpss12 4388 
Subset theorem for cross product. Generalization of Theorem 101 of
[Suppes] p. 52. (Contributed by NM,
26Aug1995.) (Proof shortened by
Andrew Salmon, 27Aug2011.)

⊢ ((A ⊆
B ∧ 𝐶 ⊆ 𝐷) → (A × 𝐶) ⊆ (B × 𝐷)) 

Theorem  xpss 4389 
A cross product is included in the ordered pair universe. Exercise 3 of
[TakeutiZaring] p. 25.
(Contributed by NM, 2Aug1994.)

⊢ (A ×
B) ⊆ (V × V) 

Theorem  relxp 4390 
A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37.
(Contributed by NM, 2Aug1994.)

⊢ Rel (A
× B) 

Theorem  xpss1 4391 
Subset relation for cross product. (Contributed by Jeff Hankins,
30Aug2009.)

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

Theorem  xpss2 4392 
Subset relation for cross product. (Contributed by Jeff Hankins,
30Aug2009.)

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

Theorem  xpsspw 4393 
A cross product is included in the power of the power of the union of
its arguments. (Contributed by NM, 13Sep2006.)

⊢ (A ×
B) ⊆ 𝒫 𝒫 (A ∪ B) 

Theorem  unixpss 4394 
The double class union of a cross product is included in the union of its
arguments. (Contributed by NM, 16Sep2006.)

⊢ ∪ ∪ (A × B) ⊆ (A
∪ B) 

Theorem  xpexg 4395 
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23. (Contributed
by NM, 14Aug1994.)

⊢ ((A ∈ 𝑉 ∧
B ∈
𝑊) → (A × B)
∈ V) 

Theorem  xpex 4396 
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23.
(Contributed by NM, 14Aug1994.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (A × B)
∈ V 

Theorem  relun 4397 
The union of two relations is a relation. Compare Exercise 5 of
[TakeutiZaring] p. 25. (Contributed
by NM, 12Aug1994.)

⊢ (Rel (A
∪ B) ↔ (Rel A ∧ Rel B)) 

Theorem  relin1 4398 
The intersection with a relation is a relation. (Contributed by NM,
16Aug1994.)

⊢ (Rel A
→ Rel (A ∩ B)) 

Theorem  relin2 4399 
The intersection with a relation is a relation. (Contributed by NM,
17Jan2006.)

⊢ (Rel B
→ Rel (A ∩ B)) 

Theorem  reldif 4400 
A difference cutting down a relation is a relation. (Contributed by NM,
31Mar1998.)

⊢ (Rel A
→ Rel (A ∖ B)) 