Type  Label  Description 
Statement 

Theorem  opelxp 4301 
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 4302 
Binary relation on a cross product. (Contributed by NM,
22Apr2004.)

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

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

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

Theorem  opelxp1 4304 
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 4305 
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 4306 
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 4307* 
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 4308 
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 4309 
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 4310 
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 4311 
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 4312 
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 4313 
No proper class is related to anything via any relation. (Contributed
by Roy F. Longton, 30Jul2005.)

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

Theorem  fconstmpt 4314* 
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 4315* 
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 4316 
Ordered pair membership in the universal class of ordered pairs.
(Contributed by Mario Carneiro, 3May2015.)

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

Theorem  opelvv 4317 
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 4318 
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 4319 
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 4320* 
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 4321* 
Membership in a cross product. (Contributed by NM, 5Mar1995.)

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

Theorem  opeliunxp 4322 
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 4323 
Distributive law for cross product over union. Theorem 103 of [Suppes]
p. 52. (Contributed by NM, 12Aug2004.)

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

Theorem  xpundir 4324 
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 4325* 
Distributive law for cross product over indexed union. (Contributed by
Mario Carneiro, 27Apr2014.)

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

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

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

Theorem  iunxpconst 4327* 
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 4328 
The cross product of two unions. (Contributed by NM, 12Aug2004.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem  opabssxp 4341* 
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 4342* 
The law of concretion for a binary relation. See brab2a 4320 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 4343* 
Implicit substitution of class for ordered pair. (Contributed by NM,
5Mar1995.)

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

Theorem  2optocl 4344* 
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 4345* 
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 4346* 
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 4347 
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 4348 
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 4349 
Equality theorem for the relation predicate. (Contributed by NM,
1Aug1994.)

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

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

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

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

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

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

⊢ ℲxA ⇒ ⊢ ℲxRel A 

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

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

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

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

Theorem  ssrel 4355* 
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 4356* 
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 4357* 
A subclass relationship depends only on a relation's ordered pairs.
This version of ssrel 4355 is restricted to the relation's domain.
(Contributed by Thierry Arnoux, 25Jan2018.)

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

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

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

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

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

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

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

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

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

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

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

Theorem  eqrelrdv 4363* 
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 4364* 
Deduction from extensionality principle for relations. (Contributed by
Mario Carneiro, 3Jan2017.)

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

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

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

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

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

Theorem  ssrelrel 4367* 
A subclass relationship determined by ordered triples. Use relrelss 4771
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 4368* 
Extensionality principle for ordered triples, analogous to eqrel 4356.
Use relrelss 4771 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 4369* 
A member of a relation is an ordered pair. (Contributed by NM,
17Sep2006.)

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

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

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

Theorem  relsnop 4371 
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 4372 
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 4373 
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 4374 
A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37.
(Contributed by NM, 2Aug1994.)

⊢ Rel (A
× B) 

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

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

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

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

Theorem  xpsspw 4377 
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 4378 
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 4379 
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 4380 
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 4381 
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 4382 
The intersection with a relation is a relation. (Contributed by NM,
16Aug1994.)

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

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

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

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

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

Theorem  reliun 4385 
An indexed union is a relation iff each member of its indexed family is
a relation. (Contributed by NM, 19Dec2008.)

⊢ (Rel ∪
x ∈
A B
↔ ∀x ∈ A Rel B) 

Theorem  reliin 4386 
An indexed intersection is a relation if at least one of the member of the
indexed family is a relation. (Contributed by NM, 8Mar2014.)

⊢ (∃x ∈ A Rel B →
Rel ∩ x
∈ A
B) 

Theorem  reluni 4387* 
The union of a class is a relation iff any member is a relation.
Exercise 6 of [TakeutiZaring] p.
25 and its converse. (Contributed by
NM, 13Aug2004.)

⊢ (Rel ∪ A ↔ ∀x ∈ A Rel
x) 

Theorem  relint 4388* 
The intersection of a class is a relation if at least one member is a
relation. (Contributed by NM, 8Mar2014.)

⊢ (∃x ∈ A Rel x →
Rel ∩ A) 

Theorem  rel0 4389 
The empty set is a relation. (Contributed by NM, 26Apr1998.)

⊢ Rel ∅ 

Theorem  relopabi 4390 
A class of ordered pairs is a relation. (Contributed by Mario Carneiro,
21Dec2013.)

⊢ A =
{⟨x, y⟩ ∣ φ} ⇒ ⊢ Rel A 

Theorem  relopab 4391 
A class of ordered pairs is a relation. (Contributed by NM, 8Mar1995.)
(Unnecessary distinct variable restrictions were removed by Alan Sare,
9Jul2013.) (Proof shortened by Mario Carneiro, 21Dec2013.)

⊢ Rel {⟨x, y⟩
∣ φ} 

Theorem  reli 4392 
The identity relation is a relation. Part of Exercise 4.12(p) of
[Mendelson] p. 235. (Contributed by
NM, 26Apr1998.) (Revised by
Mario Carneiro, 21Dec2013.)

⊢ Rel I 

Theorem  rele 4393 
The membership relation is a relation. (Contributed by NM,
26Apr1998.) (Revised by Mario Carneiro, 21Dec2013.)

⊢ Rel E 

Theorem  opabid2 4394* 
A relation expressed as an ordered pair abstraction. (Contributed by
NM, 11Dec2006.)

⊢ (Rel A
→ {⟨x, y⟩ ∣ ⟨x, y⟩
∈ A} =
A) 

Theorem  inopab 4395* 
Intersection of two ordered pair class abstractions. (Contributed by
NM, 30Sep2002.)

⊢ ({⟨x,
y⟩ ∣ φ} ∩ {⟨x, y⟩
∣ ψ}) = {⟨x, y⟩
∣ (φ ∧ ψ)} 

Theorem  difopab 4396* 
The difference of two orderedpair abstractions. (Contributed by Stefan
O'Rear, 17Jan2015.)

⊢ ({⟨x,
y⟩ ∣ φ} ∖ {⟨x, y⟩
∣ ψ}) = {⟨x, y⟩
∣ (φ ∧ ¬ ψ)} 

Theorem  inxp 4397 
The intersection of two cross products. Exercise 9 of [TakeutiZaring]
p. 25. (Contributed by NM, 3Aug1994.) (Proof shortened by Andrew
Salmon, 27Aug2011.)

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

Theorem  xpindi 4398 
Distributive law for cross product over intersection. Theorem 102 of
[Suppes] p. 52. (Contributed by NM,
26Sep2004.)

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

Theorem  xpindir 4399 
Distributive law for cross product over intersection. Similar to
Theorem 102 of [Suppes] p. 52.
(Contributed by NM, 26Sep2004.)

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

Theorem  xpiindim 4400* 
Distributive law for cross product over indexed intersection.
(Contributed by Jim Kingdon, 7Dec2018.)

⊢ (∃y y ∈ A →
(𝐶 × ∩ x ∈ A B) = ∩ x ∈ A (𝐶 × B)) 